Theorem bibi2i 337

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	bitrdi 287	. 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓))
4		id 22	. . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓))
5	4, 2	bitr4di 289	. 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑))
6	3, 5	impbii 209	1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bibi1i  338  bibi12i  339  bibi2d  342  con2bi  353  pm4.71r  558  xorass  1515  sblbis  2309  sbrbif  2311  eqabbw  2808  eqabbOLD  2875  eqabf  2928  eq0  4325  eq0rdv  4382  disj  4425  disj3  4429  rzal  4484  axrep4v  5254  axrep4  5255  axrep5  5257  axrep6  5258  axrep6OLD  5259  axsepgfromrep  5264  ax6vsep  5273  inex1  5287  axprALT  5392  zfpair2  5403  sucel  6428  suppvalbr  8163  bnj89  34752  fineqvrep  35126  axrepprim  35719  brtxpsd3  35914  bisym1  36437  bj-bixor  36609  eliminable-veqab  36884  bj-snsetex  36981  bj-reabeq  37045  bj-clex  37049  wl-3xorbi  37491  sn-axrep5v  42267  ifpidg  43515  nanorxor  44329  mo0sn  48794