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

Theorem simplbi2 608
Description: Deduction eliminating a conjunct. Automatically derived from simplbi2VD 28938. (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 197 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 423 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  simplbi2com  1364  sspss  3288  neldif  3314  reuss2  3461  pssdifn0  3528  ordunidif  4456  eceqoveq  6779  infxpenlem  7657  ackbij1lem18  7879  isf32lem2  7996  ingru  8453  indpi  8547  nqereu  8569  algcvga  12765  pcprendvds  12909  restntr  16928  filcon  17594  filssufilg  17622  ufileu  17630  ufilen  17641  alexsubALTlem3  17759  blcld  18067  causs  18740  itg2addlem  19129  rplogsum  20692  sltres  24389  intcont  25646  fdc  26558  ndmaovass  28174  onfrALTlem2  28610  3ornot23VD  28939  ordelordALTVD  28959  onfrALTlem2VD  28981  lshpcmp  29800  lfl1  29882
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 177  df-an 360
  Copyright terms: Public domain W3C validator