Theorem bibi2i 340

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	syl6bb 289	. 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓))
4		id 22	. . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓))
5	4, 2	syl6bbr 291	. 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑))
6	3, 5	impbii 211	1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi1i  341  bibi12i  342  bibi2d  345  con2bi  356  pm4.71r  561  xorass  1504  sblbis  2315  sbrbif  2317  sblbisvOLD  2325  sblbisALT  2608  abeq2  2945  abeq2f  3013  abeq2fOLD  3014  pm13.183  3658  pm13.183OLD  3659  disj3  4402  axrep5  5195  axrep6  5196  axsepgfromrep  5200  ax6vsep  5206  inex1  5220  axprALT  5322  zfpair2  5330  sucel  6263  suppvalbr  7833  bnj89  31991  axrepprim  32928  brtxpsd3  33357  bisym1  33767  bj-bixor  33925  bj-snsetex  34275  bj-reabeq  34339  sn-axrep5v  39106  ifpidg  39855  nanorxor  40635