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  4699  axsep  4703  ax6vsep  4708  inex1  4722  axpr  4827  zfpair2  4829  sucel  5701  suppvalbr  7164  bnj89  29835  bnj145OLD  29843  axrepprim  30627  brtxpsd3  30967  bisym1  31382  bj-abeq2  31755  bj-axrep5  31774  bj-axsep  31775  bj-snsetex  31938  ifpidg  36649  nanorxor  37320