Theorem bibi2i 339

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  bibi1i  340  bibi12i  341  bibi2d  344  con2bi  355  pm4.71r  559  biadanOLD  816  xorass  1500  sblbis  2284  sbrbif  2286  sblbisvOLD  2294  sblbisALT  2566  abeq2  2914  abeq2f  2981  abeq2fOLD  2982  pm13.183  3597  pm13.183OLD  3598  disj3  4317  axrep5  5087  axrep6  5088  axsepgfromrep  5092  ax6vsep  5098  inex1  5112  axprALT  5214  zfpair2  5222  sucel  6139  suppvalbr  7685  bnj89  31608  axrepprim  32536  brtxpsd3  32966  bisym1  33376  bj-abeq2  33690  bj-snsetex  33880  sn-axrep5v  38638  ifpidg  39342  nanorxor  40175