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  4333  disj3  4408  axrep4v  5231  axrep4  5232  axrep5  5234  axrep6  5235  axrep6OLD  5236  axsepgfromrep  5241  ax6vsep  5250  inex1  5264  axprALT  5369  zfpair2  5380  prex  5384  sucel  6401  tz6.12-2  6829  suppvalbr  8116  bnj89  34897  fineqvrep  35289  axrepprim  35915  brtxpsd3  36107  bisym1  36632  bj-bixor  36812  eliminable-veqab  37108  bj-snsetex  37205  bj-reabeq  37269  bj-clex  37273  bj-rep  37315  bj-axseprep  37316  wl-3xorbi  37722  sn-axrep5v  42583  ifpidg  43841  nanorxor  44655  mo0sn  49169