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

Theorem simplbi2 610
Description: Deduction eliminating a conjunct. Automatically derived from simplbi2VD 28960. (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 199 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 425 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  simplbi2com  1384  sspss  3448  neldif  3474  reuss2  3623  pssdifn0  3691  ordunidif  4631  eceqoveq  7011  infxpenlem  7897  ackbij1lem18  8119  isf32lem2  8236  ingru  8692  indpi  8786  nqereu  8808  algcvga  13072  pcprendvds  13216  restntr  17248  filcon  17917  filssufilg  17945  ufileu  17953  ufilen  17964  alexsubALTlem3  18082  blcld  18537  causs  19253  itg2addlem  19652  rplogsum  21223  sizeusglecusglem1  21495  esumpinfval  24465  sltres  25621  fdc  26451  ndmaovass  28048  elfz2z  28107  elfzmlbp  28109  elfzelfzelfz  28111  fzo1fzo0n0  28130  fzofzim  28138  swrdswrd  28201  swrdccatin1  28207  lstccats1fst  28265  cshweqdif2s  28273  usgra2pth  28313  onfrALTlem2  28634  3ornot23VD  28961  ordelordALTVD  28981  onfrALTlem2VD  29003  lshpcmp  29788  lfl1  29870
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 179  df-an 362
  Copyright terms: Public domain W3C validator