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  1544  sblbis  2341  sbrbif  2343  eqabbw  2833  eqabf  2951  ab0w  4327  disj3  4406  axrep4v  5236  axrep4  5237  axrep5  5238  axrep6  5239  zfrep6  5241  axsepgfromrep  5246  ax6vsep  5256  inex1  5276  axprALT  5383  zfpair2  5391  prex  5395  sucel  6439  tz6.12-2  6872  uniex2  7754  suppvalbr  8183  suppvalbrOLD  8184  bnj89  35398  fineqvrep  35838  vsmrep  36009  axrepprim  36559  brtxpsd3  36750  bisym1  37299  mh-infprim3bi  37428  bj-bixor  37553  eliminable-veqab  37870  bj-snsetex  37968  bj-reabeq  38032  bj-clex  38036  bj-rep  38081  bj-axseprep  38082  wl-3xorbi  38489  sn-axrep5v  43364  ifpidg  44585  nanorxor  45382  mo0sn  50020