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  2185  elres  5006  xpidtr  5081  inficl  7194  cfslb2n  7910  bezoutlem1  12733  bezoutlem3  12735  cnprest  17033  haust1  17096  lly1stc  17238  dfon2lem9  24218  inposet  25381  dfps2  25392  unint2t  25621  lppotos  26247  funcoressn  28095  ndmaovdistr  28175  3cyclfrgrarn1  28435  sb5ALT  28587  onfrALTlem2  28610  onfrALTlem2VD  28981  sb5ALTVD  29005
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