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  2345  sbrbif  2347  eqabbw  2837  eqabf  2955  ab0w  4331  disj3  4410  axrep4v  5241  axrep4  5242  axrep5  5243  axrep6  5244  zfrep6  5246  axsepgfromrep  5251  ax6vsep  5261  inex1  5282  axprALT  5389  zfpair2  5397  prex  5401  sucel  6460  tz6.12-2  6898  uniex2  7781  suppvalbr  8211  suppvalbrOLD  8212  bnj89  35435  fineqvrep  35895  vsmrep  36103  axrepprim  36658  brtxpsd3  36849  bisym1  37398  mh-infprim3bi  37527  bj-bixor  37652  eliminable-veqab  37969  bj-snsetex  38067  bj-reabeq  38131  bj-clex  38135  bj-rep  38193  bj-axseprep  38194  wl-3xorbi  38601  sn-axrep5v  43475  ifpidg  44695  nanorxor  45492  mo0sn  50142