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  2314  sbrbif  2316  eqabbw  2809  eqabf  2928  ab0w  4331  disj3  4406  axrep4v  5229  axrep4  5230  axrep5  5232  axrep6  5233  axrep6OLD  5234  axsepgfromrep  5239  ax6vsep  5248  inex1  5262  axprALT  5367  zfpair2  5378  sucel  6393  tz6.12-2  6821  suppvalbr  8106  bnj89  34877  fineqvrep  35270  axrepprim  35896  brtxpsd3  36088  bisym1  36613  bj-bixor  36791  eliminable-veqab  37067  bj-snsetex  37164  bj-reabeq  37228  bj-clex  37232  wl-3xorbi  37674  sn-axrep5v  42469  ifpidg  43728  nanorxor  44542  mo0sn  49057