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  1515  sblbis  2308  sbrbif  2310  eqabbw  2802  eqabbOLD  2868  eqabf  2921  eq0  4313  eq0rdv  4370  disj  4413  disj3  4417  rzal  4472  axrep4v  5239  axrep4  5240  axrep5  5242  axrep6  5243  axrep6OLD  5244  axsepgfromrep  5249  ax6vsep  5258  inex1  5272  axprALT  5377  zfpair2  5388  sucel  6408  suppvalbr  8143  bnj89  34711  fineqvrep  35085  axrepprim  35689  brtxpsd3  35884  bisym1  36407  bj-bixor  36579  eliminable-veqab  36854  bj-snsetex  36951  bj-reabeq  37015  bj-clex  37019  wl-3xorbi  37461  sn-axrep5v  42204  ifpidg  43480  nanorxor  44294  mo0sn  48804