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

Theorem simplbi2com 1380
Description: A deduction eliminating a conjunct, similar to simplbi2 609. (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 609 . 2  |-  ( ps 
->  ( ch  ->  ph )
)
32com12 29 1  |-  ( ch 
->  ( ps  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  mo2  2283  elres  5140  xpidtr  5215  inficl  7388  cfslb2n  8104  bezoutlem1  12993  bezoutlem3  12995  cnprest  17307  haust1  17370  lly1stc  17512  dfon2lem9  25361  funcoressn  27858  ndmaovdistr  27938  2elfz3nn0  27984  3cyclfrgrarn1  28116  sb5ALT  28320  onfrALTlem2  28343  onfrALTlem2VD  28710  sb5ALTVD  28734
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 178  df-an 361
  Copyright terms: Public domain W3C validator