Theorem bibi2i 337

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bibi1i  338  bibi12i  339  bibi2d  342  con2bi  353  pm4.71r  558  xorass  1517  sblbis  2315  sbrbif  2317  eqabbw  2809  eqabf  2928  ab0w  4319  disj3  4394  axrep4v  5217  axrep4  5218  axrep5  5220  axrep6  5221  axrep6OLD  5222  zfrep6  5224  axsepgfromrep  5229  ax6vsep  5238  inex1  5258  axprALT  5364  zfpair2  5376  prex  5380  sucel  6399  tz6.12-2  6827  suppvalbr  8114  bnj89  34864  fineqvrep  35258  axrepprim  35884  brtxpsd3  36076  bisym1  36601  mh-infprim3bi  36730  bj-bixor  36856  eliminable-veqab  37173  bj-snsetex  37270  bj-reabeq  37334  bj-clex  37338  bj-rep  37380  bj-axseprep  37381  wl-3xorbi  37789  sn-axrep5v  42658  ifpidg  43918  nanorxor  44732  mo0sn  49291