Theorem bibi2i 338

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 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  339  bibi12i  340  bibi2d  343  con2bi  354  pm4.71r  560  xorass  1515  sblbis  2306  sbrbif  2308  eqabbw  2810  eqabbOLD  2875  eqabf  2936  pm13.183  3657  dfss2  3969  eq0  4344  eq0rdv  4405  disj  4448  disj3  4454  rzal  4509  axrep5  5292  axrep6  5293  axsepgfromrep  5298  ax6vsep  5304  inex1  5318  axprALT  5421  zfpair2  5429  sucel  6439  suppvalbr  8150  bnj89  33763  fineqvrep  34126  axrepprim  34702  brtxpsd3  34899  bisym1  35352  bj-bixor  35517  eliminable-veqab  35793  bj-snsetex  35892  bj-reabeq  35956  bj-clex  35960  wl-3xorbi  36402  sn-axrep5v  41081  ifpidg  42290  nanorxor  43112  mo0sn  47548