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  2312  elres  5140  xpidtr  5215  inficl  7667  cfslb2n  8429  repswcshw  12438  cshw1  12448  bezoutlem1  13714  bezoutlem3  13716  modprmn0modprm0  13867  cnprest  18868  haust1  18931  lly1stc  19075  dfon2lem9  27555  funcoressn  29986  ndmaovdistr  30066  elovmpt2rab  30111  elovmpt2rab1  30112  2elfz3nn0  30152  3cyclfrgrarn1  30557  sb5ALT  31117  onfrALTlem2  31141  onfrALTlem2VD  31512  sb5ALTVD  31536
  Copyright terms: Public domain W3C validator