Theorem bibi2i 338

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 288	. 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓))
4		id 22	. . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓))
5	4, 2	bitr4di 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  339  bibi12i  340  bibi2d  343  con2bi  354  pm4.71r  563  xorass  1522  sblbis  2319  sbrbif  2321  eqabbw  2813  eqabf  2931  ab0w  4314  disj3  4389  axrep4v  5211  axrep4  5212  axrep5  5214  axrep6  5215  axrep6OLD  5216  zfrep6  5218  axsepgfromrep  5223  ax6vsep  5232  inex1  5252  axprALT  5358  zfpair2  5370  prex  5374  sucel  6393  tz6.12-2  6821  suppvalbr  8111  bnj89  34911  fineqvrep  35302  axrepprim  35937  brtxpsd3  36129  bisym1  36654  mh-infprim3bi  36783  bj-bixor  36909  eliminable-veqab  37226  bj-snsetex  37323  bj-reabeq  37387  bj-clex  37391  bj-rep  37433  bj-axseprep  37434  wl-3xorbi  37842  sn-axrep5v  42711  ifpidg  43942  nanorxor  44756  mo0sn  49313