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

Theorem simplbi2com 627
Description: A deduction eliminating a conjunct, similar to simplbi2 625. (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 625 . 2  |-  ( ps 
->  ( ch  ->  ph )
)
32com12 31 1  |-  ( ch 
->  ( ps  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mo2OLD  2323  elres  5256  xpidtr  5331  inficl  7789  cfslb2n  8551  repswcshw  12567  cshw1  12577  bezoutlem1  13843  bezoutlem3  13845  modprmn0modprm0  13996  cnprest  19028  haust1  19091  lly1stc  19235  dfon2lem9  27768  funcoressn  30201  ndmaovdistr  30281  elovmpt2rab  30326  elovmpt2rab1  30327  2elfz3nn0  30367  3cyclfrgrarn1  30772  sb5ALT  31582  onfrALTlem2  31606  onfrALTlem2VD  31977  sb5ALTVD  32001
  Copyright terms: Public domain W3C validator