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

Theorem sylanr1 650
Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.)
Hypotheses
Ref Expression
sylanr1.1  |-  ( ph  ->  ch )
sylanr1.2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
Assertion
Ref Expression
sylanr1  |-  ( ( ps  /\  ( ph  /\ 
th ) )  ->  ta )

Proof of Theorem sylanr1
StepHypRef Expression
1 sylanr1.1 . . 3  |-  ( ph  ->  ch )
21anim1i 566 . 2  |-  ( (
ph  /\  th )  ->  ( ch  /\  th ) )
3 sylanr1.2 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
42, 3sylan2 472 1  |-  ( ( ps  /\  ( ph  /\ 
th ) )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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:  adantrll  719  adantrlr  720  sbthlem9  7628  pczpre  14455  cpmadugsumlemF  19544  blsscls2  21173  rpvmasumlem  23870  leopmuli  27250  chirredlem1  27507  chirredlem3  27509  dvconstbi  31480  bccbc  31491  reccot  33542  rectan  33543  aacllem  33604
  Copyright terms: Public domain W3C validator