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  1516  sblbis  2312  sbrbif  2314  eqabbw  2806  eqabf  2925  ab0w  4328  disj3  4403  axrep4v  5224  axrep4  5225  axrep5  5227  axrep6  5228  axrep6OLD  5229  axsepgfromrep  5234  ax6vsep  5243  inex1  5257  axprALT  5362  zfpair2  5373  sucel  6387  tz6.12-2  6815  suppvalbr  8100  bnj89  34754  fineqvrep  35158  axrepprim  35767  brtxpsd3  35959  bisym1  36484  bj-bixor  36656  eliminable-veqab  36931  bj-snsetex  37028  bj-reabeq  37092  bj-clex  37096  wl-3xorbi  37538  sn-axrep5v  42335  ifpidg  43609  nanorxor  44423  mo0sn  48941