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

Theorem simplbi2 609
Description: Deduction eliminating a conjunct. Automatically derived from simplbi2VD 28667. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
pm3.26bi2.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi2  |-  ( ps 
->  ( ch  ->  ph )
)

Proof of Theorem simplbi2
StepHypRef Expression
1 pm3.26bi2.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpri 198 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 424 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  simplbi2com  1380  sspss  3406  neldif  3432  reuss2  3581  pssdifn0  3649  ordunidif  4589  eceqoveq  6968  infxpenlem  7851  ackbij1lem18  8073  isf32lem2  8190  ingru  8646  indpi  8740  nqereu  8762  algcvga  13025  pcprendvds  13169  restntr  17200  filcon  17868  filssufilg  17896  ufileu  17904  ufilen  17915  alexsubALTlem3  18033  blcld  18488  causs  19204  itg2addlem  19603  rplogsum  21174  sizeusglecusglem1  21446  esumpinfval  24416  sltres  25532  fdc  26339  ndmaovass  27937  elfzmlbp  27978  elfzelfzelfz  27981  fzo1fzo0n0  27988  swrdswrd  28011  swrdccatin1  28016  swrdccatin12b  28027  usgra2pth  28041  onfrALTlem2  28343  3ornot23VD  28668  ordelordALTVD  28688  onfrALTlem2VD  28710  lshpcmp  29471  lfl1  29553
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator