Theorem bibi2i 327

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  bibi1i  328  bibi12i  329  bibi2d  332  con2bi  343  pm4.71r  662  xorass  1465  sblbis  2403  sbrbif  2405  abeq2  2729  abeq2f  2788  pm13.183  3332  symdifass  3837  disj3  3999  euabsn2  4237  axrep5  4746  axsep  4750  ax6vsep  4755  inex1  4769  axpr  4876  zfpair2  4878  sucel  5767  suppvalbr  7259  bnj89  30548  bnj145OLD  30556  axrepprim  31340  brtxpsd3  31698  bisym1  32113  bj-abeq2  32469  bj-axrep5  32488  bj-axsep  32489  bj-snsetex  32651  ifpidg  37356  nanorxor  38025