Theorem bibi2i 340

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi1i  341  bibi12i  342  bibi2d  345  con2bi  356  pm4.71r  561  xorass  1506  sblbis  2319  sbrbif  2321  sblbisvOLD  2329  sblbisALT  2612  abeq2  2947  abeq2f  3015  abeq2fOLD  3016  pm13.183  3661  pm13.183OLD  3662  disj3  4405  axrep5  5198  axrep6  5199  axsepgfromrep  5203  ax6vsep  5209  inex1  5223  axprALT  5325  zfpair2  5333  sucel  6266  suppvalbr  7836  bnj89  31993  axrepprim  32930  brtxpsd3  33359  bisym1  33769  bj-bixor  33927  bj-snsetex  34277  bj-reabeq  34341  sn-axrep5v  39115  ifpidg  39864  nanorxor  40644