Theorem bibi2i 327

Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)

Hypothesis

Ref	Expression
bibi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
bibi2i	⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

Proof of Theorem bibi2i

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜑))
2		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	syl6bb 276	. 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓))
4		id 22	. . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓))
5	4, 2	syl6bbr 278	. 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑))
6	3, 5	impbii 199	1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

Syntax hints:   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  bibi1i  328  bibi12i  329  bibi2d  332  con2bi  343  pm4.71r  663  xorass  1468  sblbis  2404  sbrbif  2406  abeq2  2732  abeq2f  2792  pm13.183  3344  symdifass  3853  disj3  4021  euabsn2  4260  axrep5  4776  axsep  4780  ax6vsep  4785  inex1  4799  axpr  4905  zfpair2  4907  sucel  5798  suppvalbr  7299  bnj89  30787  bnj145OLD  30795  axrepprim  31579  brtxpsd3  32003  bisym1  32418  bj-abeq2  32773  bj-axrep5  32792  bj-axsep  32793  bj-snsetex  32951  ifpidg  37836  nanorxor  38504