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 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bibi1i  341  bibi12i  342  bibi2d  345  con2bi  356  pm4.71r  567  xorass  1538  sblbis  2345  sbrbif  2347  eqabbw  2838  eqabf  2956  ab0w  4335  disj3  4411  axrep4v  5237  axrep4  5238  axrep5  5240  axrep6  5241  axrep6OLD  5242  zfrep6  5244  axsepgfromrep  5249  ax6vsep  5258  inex1  5278  axprALT  5384  zfpair2  5396  prex  5400  sucel  6426  tz6.12-2  6858  suppvalbr  8148  bnj89  35027  fineqvrep  35422  axrepprim  36065  brtxpsd3  36257  bisym1  36792  mh-infprim3bi  36921  bj-bixor  37046  eliminable-veqab  37363  bj-snsetex  37460  bj-reabeq  37524  bj-clex  37528  bj-rep  37570  bj-axseprep  37571  wl-3xorbi  37979  sn-axrep5v  42848  ifpidg  44079  nanorxor  44879  mo0sn  49445