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

Theorem syl331anc 1253
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
sylXanc.6  |-  ( ph  ->  ze )
sylXanc.7  |-  ( ph  ->  si )
syl331anc.8  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  si )  ->  rh )
Assertion
Ref Expression
syl331anc  |-  ( ph  ->  rh )

Proof of Theorem syl331anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
6 sylXanc.6 . . 3  |-  ( ph  ->  ze )
74, 5, 63jca 1176 . 2  |-  ( ph  ->  ( ta  /\  et  /\  ze ) )
8 sylXanc.7 . 2  |-  ( ph  ->  si )
9 syl331anc.8 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  si )  ->  rh )
101, 2, 3, 7, 8, 9syl311anc 1242 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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  df-3an 975
This theorem is referenced by:  syl332anc  1259  syl333anc  1260  qredeu  14351  brbtwn2  24426  3atlem4  35396  3atlem6  35398  llnexchb2  35779  osumcllem9N  35874  cdlemd4  36112  cdleme26fALTN  36274  cdleme26f  36275  cdleme36m  36373  cdlemg17b  36574  cdlemg17h  36580  cdlemk38  36827  cdlemk53b  36868  cdlemkyyN  36874  cdlemk43N  36875
  Copyright terms: Public domain W3C validator