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  1615  sblbis  2539  sbrbif  2541  abeq2  2868  abeq2f  2928  pm13.183  3482  symdifass  3994  disj3  4162  euabsn2  4402  axrep5  4926  axsep  4930  ax6vsep  4935  inex1  4949  axpr  5052  zfpair2  5054  sucel  5957  suppvalbr  7465  bnj89  31094  axrepprim  31884  brtxpsd3  32307  bisym1  32722  bj-abeq2  33077  bj-axrep5  33096  bj-axsep  33097  bj-snsetex  33255  ifpidg  38336  nanorxor  39004