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  2309  sbrbif  2311  eqabbw  2815  eqabbOLD  2882  eqabf  2935  eq0  4350  eq0rdv  4407  disj  4450  disj3  4454  rzal  4509  axrep4v  5284  axrep4  5285  axrep5  5287  axrep6  5288  axrep6OLD  5289  axsepgfromrep  5294  ax6vsep  5303  inex1  5317  axprALT  5422  zfpair2  5433  sucel  6458  suppvalbr  8189  bnj89  34735  fineqvrep  35109  axrepprim  35702  brtxpsd3  35897  bisym1  36420  bj-bixor  36592  eliminable-veqab  36867  bj-snsetex  36964  bj-reabeq  37028  bj-clex  37032  wl-3xorbi  37474  sn-axrep5v  42255  ifpidg  43504  nanorxor  44324  mo0sn  48735