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  4303  eq0rdv  4360  disj  4403  disj3  4407  rzal  4462  axrep4v  5226  axrep4  5227  axrep5  5229  axrep6  5230  axrep6OLD  5231  axsepgfromrep  5236  ax6vsep  5245  inex1  5259  axprALT  5364  zfpair2  5375  sucel  6387  suppvalbr  8104  bnj89  34690  fineqvrep  35072  axrepprim  35677  brtxpsd3  35872  bisym1  36395  bj-bixor  36567  eliminable-veqab  36842  bj-snsetex  36939  bj-reabeq  37003  bj-clex  37007  wl-3xorbi  37449  sn-axrep5v  42192  ifpidg  43467  nanorxor  44281  mo0sn  48804