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

Theorem simplbi2com 625
Description: A deduction eliminating a conjunct, similar to simplbi2 623. (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 623 . 2  |-  ( ps 
->  ( ch  ->  ph )
)
32com12 31 1  |-  ( ch 
->  ( ps  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  elres  5297  xpidtr  5377  elovmpt2rab  6494  elovmpt2rab1  6495  inficl  7877  cfslb2n  8639  repswcshw  12771  cshw1  12781  bezoutlem1  14260  bezoutlem3  14262  modprmn0modprm0  14416  cnprest  19957  haust1  20020  lly1stc  20163  3cyclfrgrarn1  25214  dfon2lem9  29463  funcoressn  32451  ndmaovdistr  32531  reuccatpfxs1  32662  2elfz3nn0  32706  sb5ALT  33682  onfrALTlem2  33712  onfrALTlem2VD  34090  sb5ALTVD  34114
  Copyright terms: Public domain W3C validator