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  1545  sblbis  2343  sbrbif  2345  eqabbw  2836  eqabf  2954  ab0w  4336  disj3  4415  axrep4v  5244  axrep4  5245  axrep5  5247  axrep6  5248  axrep6OLD  5249  zfrep6  5251  axsepgfromrep  5256  ax6vsep  5267  inex1  5287  axprALT  5395  zfpair2  5407  prex  5411  sucel  6439  tz6.12-2  6870  uniex2  7737  suppvalbr  8161  bnj89  35088  fineqvrep  35505  axrepprim  36172  brtxpsd3  36364  bisym1  36908  mh-infprim3bi  37037  bj-bixor  37162  eliminable-veqab  37479  bj-snsetex  37577  bj-reabeq  37641  bj-clex  37645  bj-rep  37688  bj-axseprep  37689  wl-3xorbi  38097  sn-axrep5v  42966  ifpidg  44197  nanorxor  44995  mo0sn  49571