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

Theorem simplbi2com 1384
Description: A deduction eliminating a conjunct, similar to simplbi2 610. (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 610 . 2  |-  ( ps 
->  ( ch  ->  ph )
)
32com12 30 1  |-  ( ch 
->  ( ps  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  mo2  2312  elres  5183  xpidtr  5258  inficl  7432  cfslb2n  8150  bezoutlem1  13040  bezoutlem3  13042  cnprest  17355  haust1  17418  lly1stc  17561  dfon2lem9  25420  funcoressn  27969  ndmaovdistr  28049  elovmpt2rab  28092  elovmpt2rab1  28093  2elfz3nn0  28123  cshw1  28297  3cyclfrgrarn1  28464  sb5ALT  28671  onfrALTlem2  28694  onfrALTlem2VD  29063  sb5ALTVD  29087
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 179  df-an 362
  Copyright terms: Public domain W3C validator