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  1511  sblbis  2307  sbrbif  2309  eqabbw  2812  eqabbOLD  2879  eqabf  2932  eq0  4355  eq0rdv  4412  disj  4455  disj3  4459  rzal  4514  axrep4v  5289  axrep4  5290  axrep5  5292  axrep6  5293  axrep6OLD  5294  axsepgfromrep  5299  ax6vsep  5308  inex1  5322  axprALT  5427  zfpair2  5438  sucel  6459  suppvalbr  8187  bnj89  34713  fineqvrep  35087  axrepprim  35681  brtxpsd3  35877  bisym1  36401  bj-bixor  36573  eliminable-veqab  36848  bj-snsetex  36945  bj-reabeq  37009  bj-clex  37013  wl-3xorbi  37455  sn-axrep5v  42233  ifpidg  43480  nanorxor  44300  mo0sn  48663