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  2310  sbrbif  2312  eqabbw  2804  eqabbOLD  2871  eqabf  2924  eq0  4300  eq0rdv  4357  disj3  4404  rzal  4459  axrep4v  5222  axrep4  5223  axrep5  5225  axrep6  5226  axrep6OLD  5227  axsepgfromrep  5232  ax6vsep  5241  inex1  5255  axprALT  5360  zfpair2  5371  sucel  6382  tz6.12-2  6809  suppvalbr  8094  bnj89  34731  fineqvrep  35135  axrepprim  35744  brtxpsd3  35936  bisym1  36459  bj-bixor  36631  eliminable-veqab  36906  bj-snsetex  37003  bj-reabeq  37067  bj-clex  37071  wl-3xorbi  37513  sn-axrep5v  42255  ifpidg  43530  nanorxor  44344  mo0sn  48853