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

Theorem simplbi2 656
Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
simplbi2.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
simplbi2 (𝜓 → (𝜒𝜑))

Proof of Theorem simplbi2
StepHypRef Expression
1 simplbi2.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21biimpri 218 . 2 ((𝜓𝜒) → 𝜑)
32ex 449 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  simplbi2com  658  sspss  3840  neldif  3870  reuss2  4042  pssdifn0  4079  ordunidif  5926  eceqoveq  8011  infxpenlem  9018  ackbij1lem18  9243  isf32lem2  9360  ingru  9821  indpi  9913  nqereu  9935  elfz0ubfz0  12629  elfzmlbp  12636  elfzo0z  12696  fzofzim  12701  fzo1fzo0n0  12705  elfzodifsumelfzo  12720  ccat1st1st  13594  2swrd1eqwrdeq  13646  swrdswrd  13652  swrdccatin1  13675  swrd2lsw  13888  p1modz1  15181  dfgcd2  15457  algcvga  15486  pcprendvds  15739  restntr  21180  filconn  21880  filssufilg  21908  ufileu  21916  ufilen  21927  alexsubALTlem3  22046  blcld  22503  causs  23288  itg2addlem  23716  rplogsum  25407  wlkonl1iedg  26763  trlf1  26797  spthdifv  26831  upgrwlkdvde  26835  usgr2pth  26862  pthdlem2  26866  uspgrn2crct  26903  crctcshwlkn0  26916  clwlkclwwlklem2  27115  clwwlknon0  27232  3spthd  27320  ofpreima2  29767  esumpinfval  30436  eulerpartlemf  30733  sltres  32113  bj-elid2  33389  fin2so  33701  fdc  33846  lshpcmp  34770  lfl1  34852  frege124d  38547  onfrALTlem2  39255  3ornot23VD  39573  ordelordALTVD  39594  onfrALTlem2VD  39616  ndmaovass  41784  elfz2z  41827  lighneallem4  42029
  Copyright terms: Public domain W3C validator