Theorem bibi2i 326

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  327  bibi12i  328  bibi2d  331  con2bi  342  pm4.71r  666  xorass  1617  sblbis  2542  sbrbif  2544  abeq2  2871  abeq2f  2931  pm13.183  3485  symdifass  3997  disj3  4165  euabsn2  4405  axrep5  4929  axsep  4933  ax6vsep  4938  inex1  4952  axpr  5055  zfpair2  5057  sucel  5960  suppvalbr  7469  bnj89  31118  axrepprim  31908  brtxpsd3  32331  bisym1  32746  bj-abeq2  33102  bj-axrep5  33121  bj-axsep  33122  bj-snsetex  33276  ifpidg  38357  nanorxor  39025