MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi2i Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 id 22 . . 3 ((𝜒𝜑) → (𝜒𝜑))
2 bibi2i.1 . . 3 (𝜑𝜓)
31, 2bitrdi 287 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 22 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2bitr4di 289 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 208 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205
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 206
This theorem is referenced by:  bibi1i  339  bibi12i  340  bibi2d  343  con2bi  354  pm4.71r  560  xorass  1515  sblbis  2306  sbrbif  2308  eqabw  2814  eqabOLD  2879  eqabf  2941  pm13.183  3619  dfss2  3931  eq0  4304  eq0rdv  4365  disj  4408  disj3  4414  rzal  4467  axrep5  5249  axrep6  5250  axsepgfromrep  5255  ax6vsep  5261  inex1  5275  axprALT  5378  zfpair2  5386  sucel  6392  suppvalbr  8097  bnj89  33336  fineqvrep  33699  axrepprim  34276  brtxpsd3  34484  bisym1  34894  bj-bixor  35059  eliminable-veqab  35335  bj-snsetex  35437  bj-reabeq  35501  bj-clex  35505  wl-3xorbi  35947  sn-axrep5v  40641  ifpidg  41770  nanorxor  42592  mo0sn  46907
  Copyright terms: Public domain W3C validator