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

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  bibi1i  327  bibi12i  328  bibi2d  331  con2bi  342  pm4.71r  661  xorass  1460  sblbis  2392  sbrbif  2394  abeq2  2719  abeq2f  2778  pm13.183  3313  symdifass  3815  disj3  3973  euabsn2  4204  axrep5  4704  axsep  4708  ax6vsep  4713  inex1  4727  axpr  4832  zfpair2  4834  sucel  5715  suppvalbr  7186  bnj89  30041  bnj145OLD  30049  axrepprim  30833  brtxpsd3  31173  bisym1  31588  bj-abeq2  31961  bj-axrep5  31980  bj-axsep  31981  bj-snsetex  32144  ifpidg  36855  nanorxor  37526