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  2336  elres  5315  xpidtr  5395  elovmpt2rab  6516  elovmpt2rab1  6517  inficl  7897  cfslb2n  8660  repswcshw  12760  cshw1  12770  bezoutlem1  14052  bezoutlem3  14054  modprmn0modprm0  14208  cnprest  19658  haust1  19721  lly1stc  19865  3cyclfrgrarn1  24826  dfon2lem9  29141  funcoressn  31993  ndmaovdistr  32073  2elfz3nn0  32113  sb5ALT  32730  onfrALTlem2  32754  onfrALTlem2VD  33125  sb5ALTVD  33149
  Copyright terms: Public domain W3C validator