Theorem bibi2i 340

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 23	. . 3 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜑))
2		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	bitrdi 290	. 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓))
4		id 23	. . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓))
5	4, 2	bitr4di 292	. 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑))
6	3, 5	impbii 212	1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1i  341  bibi12i  342  bibi2d  345  con2bi  356  pm4.71r  568  xorass  1545  sblbis  2346  sbrbif  2348  eqabbw  2839  eqabf  2957  ab0w  4338  disj3  4417  axrep4v  5248  axrep4  5249  axrep5  5251  axrep6  5252  axrep6OLD  5253  zfrep6  5255  axsepgfromrep  5260  ax6vsep  5271  inex1  5291  axprALT  5398  zfpair2  5410  prex  5414  sucel  6444  tz6.12-2  6875  uniex2  7748  suppvalbr  8169  bnj89  35142  fineqvrep  35551  axrepprim  36215  brtxpsd3  36407  bisym1  36971  mh-infprim3bi  37100  bj-bixor  37225  eliminable-veqab  37542  bj-snsetex  37640  bj-reabeq  37704  bj-clex  37708  bj-rep  37751  bj-axseprep  37752  wl-3xorbi  38160  sn-axrep5v  43029  ifpidg  44258  nanorxor  45056  mo0sn  49635