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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  bibi1i  338  bibi12i  339  bibi2d  342  con2bi  353  pm4.71r  559  xorass  1514  sblbis  2305  sbrbif  2307  eqabbw  2809  eqabbOLD  2874  eqabf  2935  pm13.183  3656  dfss2  3968  eq0  4343  eq0rdv  4404  disj  4447  disj3  4453  rzal  4508  axrep5  5291  axrep6  5292  axsepgfromrep  5297  ax6vsep  5303  inex1  5317  axprALT  5420  zfpair2  5428  sucel  6438  suppvalbr  8149  bnj89  33727  fineqvrep  34090  axrepprim  34666  brtxpsd3  34863  bisym1  35299  bj-bixor  35464  eliminable-veqab  35740  bj-snsetex  35839  bj-reabeq  35903  bj-clex  35907  wl-3xorbi  36349  sn-axrep5v  41035  ifpidg  42232  nanorxor  43054  mo0sn  47490