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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  bibi1i  338  bibi12i  339  bibi2d  342  con2bi  353  pm4.71r  558  xorass  1508  sblbis  2309  sbrbif  2311  abeq2w  2816  abeq2  2871  abeq2f  2939  pm13.183  3590  dfss2  3903  eq0  4274  eq0rdv  4335  disj  4378  disj3  4384  rzal  4436  axrep5  5211  axrep6  5212  axsepgfromrep  5216  ax6vsep  5222  inex1  5236  axprALT  5340  zfpair2  5348  sucel  6324  suppvalbr  7952  bnj89  32600  fineqvrep  32964  axrepprim  33543  brtxpsd3  34125  bisym1  34535  bj-bixor  34700  eliminable-veqab  34977  bj-snsetex  35080  bj-reabeq  35144  wl-3xorbi  35571  sn-axrep5v  40113  ifpidg  40996  nanorxor  41812  mo0sn  46049