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

Theorem simplbi2 622
Description: Deduction eliminating a conjunct. Automatically derived from simplbi2VD 31416. (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 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  1422  sspss  3452  neldif  3478  reuss2  3627  pssdifn0  3737  ordunidif  4763  eceqoveq  7201  infxpenlem  8176  ackbij1lem18  8402  isf32lem2  8519  ingru  8978  indpi  9072  nqereu  9094  elfzelfzelfz  11480  elfzmlbp  11487  fzo1fzo0n0  11584  elfzo0z  11585  fzofzim  11589  elfzodifsumelfzo  11600  ccatval1lsw  12279  2swrd1eqwrdeq  12344  swrdswrd  12350  swrdccatin1  12370  swrd2lsw  12548  algcvga  13750  pcprendvds  13903  restntr  18745  filcon  19415  filssufilg  19443  ufileu  19451  ufilen  19462  alexsubALTlem3  19580  blcld  20039  causs  20768  itg2addlem  21195  rplogsum  22735  sizeusglecusglem1  23327  esumpinfval  26458  eulerpartlemf  26683  sltres  27734  fin2so  28341  fdc  28566  ndmaovass  30037  elfz2z  30123  ccats1rev  30185  usgra2pth  30226  clwlkisclwwlklem1  30374  clwwlknwwlkncl  30387  numclwwlk2lem1  30620  onfrALTlem2  31087  3ornot23VD  31417  ordelordALTVD  31437  onfrALTlem2VD  31459  lshpcmp  32355  lfl1  32437
  Copyright terms: Public domain W3C validator