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  1517  sblbis  2315  sbrbif  2317  eqabbw  2810  eqabf  2929  ab0w  4333  disj3  4408  axrep4v  5231  axrep4  5232  axrep5  5234  axrep6  5235  axrep6OLD  5236  zfrep6  5238  axsepgfromrep  5243  ax6vsep  5252  inex1  5266  axprALT  5371  zfpair2  5382  prex  5386  sucel  6403  tz6.12-2  6831  suppvalbr  8118  bnj89  34904  fineqvrep  35298  axrepprim  35924  brtxpsd3  36116  bisym1  36641  bj-bixor  36824  eliminable-veqab  37141  bj-snsetex  37238  bj-reabeq  37302  bj-clex  37306  bj-rep  37348  bj-axseprep  37349  wl-3xorbi  37755  sn-axrep5v  42618  ifpidg  43876  nanorxor  44690  mo0sn  49204