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

Theorem simplbi2 635
Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
simplbi2.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi2  |-  ( ps 
->  ( ch  ->  ph )
)

Proof of Theorem simplbi2
StepHypRef Expression
1 simplbi2.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpri 211 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 440 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  simplbi2com  637  sspss  3543  neldif  3569  reuss2  3734  pssdifn0  3838  ordunidif  5489  eceqoveq  7493  infxpenlem  8469  ackbij1lem18  8692  isf32lem2  8809  ingru  9265  indpi  9357  nqereu  9379  elfz0ubfz0  11923  elfzmlbp  11931  fzo1fzo0n0  11987  elfzo0z  11988  fzofzim  11992  elfzodifsumelfzo  12010  2swrd1eqwrdeq  12846  swrdswrd  12852  swrdccatin1  12875  swrd2lsw  13075  algcvga  14586  pcprendvds  14838  restntr  20246  filcon  20946  filssufilg  20974  ufileu  20982  ufilen  20993  alexsubALTlem3  21112  blcld  21568  causs  22316  itg2addlem  22764  rplogsum  24413  sizeusglecusglem1  25260  clwlkisclwwlklem1  25563  clwwlknwwlkncl  25576  numclwwlk2lem1  25878  ofpreima2  28317  esumpinfval  28942  eulerpartlemf  29251  sltres  30599  bj-elid2  31685  fin2so  31976  fdc  32118  lshpcmp  32598  lfl1  32680  frege124d  36397  onfrALTlem2  36955  3ornot23VD  37282  ordelordALTVD  37303  onfrALTlem2VD  37325  ndmaovass  38745  elfz2z  39096  upgrwlkdvde  39768  pthdlem2  39793  uspgrn2crct  39825  3spthd  39916  usgra2pth  39940
  Copyright terms: Public domain W3C validator