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  3470  neldif  3496  reuss2  3645  pssdifn0  3755  ordunidif  4782  eceqoveq  7220  infxpenlem  8195  ackbij1lem18  8421  isf32lem2  8538  ingru  8997  indpi  9091  nqereu  9113  elfzelfzelfz  11499  elfzmlbp  11506  fzo1fzo0n0  11603  elfzo0z  11604  fzofzim  11608  elfzodifsumelfzo  11619  ccatval1lsw  12298  2swrd1eqwrdeq  12363  swrdswrd  12369  swrdccatin1  12389  swrd2lsw  12567  algcvga  13769  pcprendvds  13922  restntr  18801  filcon  19471  filssufilg  19499  ufileu  19507  ufilen  19518  alexsubALTlem3  19636  blcld  20095  causs  20824  itg2addlem  21251  rplogsum  22791  sizeusglecusglem1  23407  esumpinfval  26537  eulerpartlemf  26768  sltres  27820  fin2so  28435  fdc  28660  ndmaovass  30131  elfz2z  30217  ccats1rev  30279  usgra2pth  30320  clwlkisclwwlklem1  30468  clwwlknwwlkncl  30481  numclwwlk2lem1  30714  onfrALTlem2  31273  3ornot23VD  31602  ordelordALTVD  31622  onfrALTlem2VD  31644  lshpcmp  32652  lfl1  32734
  Copyright terms: Public domain W3C validator