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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bibi1i  338  bibi12i  339  bibi2d  342  con2bi  353  pm4.71r  558  xorass  1517  sblbis  2315  sbrbif  2317  eqabbw  2810  eqabf  2929  ab0w  4320  disj3  4395  axrep4v  5217  axrep4  5218  axrep5  5220  axrep6  5221  axrep6OLD  5222  zfrep6  5224  axsepgfromrep  5229  ax6vsep  5238  inex1  5254  axprALT  5359  zfpair2  5371  prex  5375  sucel  6393  tz6.12-2  6821  suppvalbr  8107  bnj89  34880  fineqvrep  35274  axrepprim  35900  brtxpsd3  36092  bisym1  36617  mh-infprim3bi  36746  bj-bixor  36872  eliminable-veqab  37189  bj-snsetex  37286  bj-reabeq  37350  bj-clex  37354  bj-rep  37396  bj-axseprep  37397  wl-3xorbi  37803  sn-axrep5v  42672  ifpidg  43936  nanorxor  44750  mo0sn  49303