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

Theorem simplbi2com 1364
Description: A deduction eliminating a conjunct, similar to simplbi2 608. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)
Hypothesis
Ref Expression
simplbi2com.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi2com  |-  ( ch 
->  ( ps  ->  ph )
)

Proof of Theorem simplbi2com
StepHypRef Expression
1 simplbi2com.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21simplbi2 608 . 2  |-  ( ps 
->  ( ch  ->  ph )
)
32com12 27 1  |-  ( ch 
->  ( ps  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  mo2  2172  elres  4990  xpidtr  5065  inficl  7178  cfslb2n  7894  bezoutlem1  12717  bezoutlem3  12719  cnprest  17017  haust1  17080  lly1stc  17222  dfon2lem9  24147  inposet  25278  dfps2  25289  unint2t  25518  lppotos  26144  funcoressn  27990  ndmaovdistr  28067  sb5ALT  28288  onfrALTlem2  28311  onfrALTlem2VD  28665  sb5ALTVD  28689
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