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

Theorem simplbi2 625
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 206 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 434 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  simplbi2com  627  sspss  3603  neldif  3629  reuss2  3778  pssdifn0  3888  ordunidif  4926  eceqoveq  7413  infxpenlem  8387  ackbij1lem18  8613  isf32lem2  8730  ingru  9189  indpi  9281  nqereu  9303  elfz0ubfz0  11772  elfzmlbp  11779  fzo1fzo0n0  11828  elfzo0z  11829  fzofzim  11833  elfzodifsumelfzo  11846  ccatval1lsw  12563  2swrd1eqwrdeq  12638  swrdswrd  12644  swrdccatin1  12667  swrd2lsw  12849  algcvga  14063  pcprendvds  14219  restntr  19449  filcon  20119  filssufilg  20147  ufileu  20155  ufilen  20166  alexsubALTlem3  20284  blcld  20743  causs  21472  itg2addlem  21900  rplogsum  23440  sizeusglecusglem1  24160  clwlkisclwwlklem1  24463  clwwlknwwlkncl  24476  numclwwlk2lem1  24779  esumpinfval  27719  eulerpartlemf  27949  sltres  29001  fin2so  29617  fdc  29841  ndmaovass  31758  elfz2z  31800  usgra2pth  31823  onfrALTlem2  32398  3ornot23VD  32727  ordelordALTVD  32747  onfrALTlem2VD  32769  bj-elid2  33673  lshpcmp  33785  lfl1  33867
  Copyright terms: Public domain W3C validator