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 23	. . 3 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜑))
2		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	bitrdi 290	. 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓))
4		id 23	. . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓))
5	4, 2	bitr4di 292	. 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑))
6	3, 5	impbii 212	1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1i  341  bibi12i  342  bibi2d  345  con2bi  356  pm4.71r  568  xorass  1545  sblbis  2342  sbrbif  2344  eqabbw  2834  eqabf  2952  ab0w  4328  disj3  4407  axrep4v  5237  axrep4  5238  axrep5  5239  axrep6  5240  zfrep6  5242  axsepgfromrep  5247  ax6vsep  5257  inex1  5277  axprALT  5384  zfpair2  5392  prex  5396  sucel  6432  tz6.12-2  6864  uniex2  7743  suppvalbr  8165  bnj89  35335  fineqvrep  35755  axrepprim  36436  brtxpsd3  36628  bisym1  37177  mh-infprim3bi  37306  bj-bixor  37431  eliminable-veqab  37748  bj-snsetex  37846  bj-reabeq  37910  bj-clex  37914  bj-rep  37957  bj-axseprep  37958  wl-3xorbi  38364  sn-axrep5v  43239  ifpidg  44450  nanorxor  45248  mo0sn  49870