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  2343  sbrbif  2345  eqabbw  2835  eqabf  2953  ab0w  4331  disj3  4410  axrep4v  5241  axrep4  5242  axrep5  5244  axrep6  5245  axrep6OLD  5246  zfrep6  5248  axsepgfromrep  5253  ax6vsep  5264  inex1  5284  axprALT  5391  zfpair2  5403  prex  5407  sucel  6438  tz6.12-2  6869  uniex2  7743  suppvalbr  8166  bnj89  35239  fineqvrep  35648  axrepprim  36289  brtxpsd3  36481  bisym1  37046  mh-infprim3bi  37175  bj-bixor  37300  eliminable-veqab  37617  bj-snsetex  37715  bj-reabeq  37779  bj-clex  37783  bj-rep  37826  bj-axseprep  37827  wl-3xorbi  38235  sn-axrep5v  43095  ifpidg  44339  nanorxor  45137  mo0sn  49752