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

Theorem simplbi2com 631
Description: A deduction eliminating a conjunct, similar to simplbi2 629. (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 629 . 2  |-  ( ps 
->  ( ch  ->  ph )
)
32com12 32 1  |-  ( ch 
->  ( ps  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  elres  5102  xpidtr  5184  elovmpt2rab  6473  elovmpt2rab1  6474  inficl  7892  cfslb2n  8649  repswcshw  12857  cshw1  12867  bezoutlem1  14446  bezoutlem3OLD  14448  bezoutlem3  14451  modprmn0modprm0  14701  cnprest  20247  haust1  20310  lly1stc  20453  3cyclfrgrarn1  25682  dfon2lem9  30388  phpreu  31836  poimirlem26  31873  sb5ALT  36795  onfrALTlem2  36825  onfrALTlem2VD  37202  sb5ALTVD  37226  funcoressn  38442  ndmaovdistr  38522  reuccatpfxs1  38788  2elfz3nn0  38853
  Copyright terms: Public domain W3C validator