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

Theorem syl331anc 1207
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 1132 . 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 1196 1  |-  ( ph  ->  rh )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl332anc  1213  syl333anc  1214  qredeu  12786  brbtwn2  24533  3atlem4  29675  3atlem6  29677  llnexchb2  30058  osumcllem9N  30153  cdlemd4  30390  cdleme26fALTN  30551  cdleme26f  30552  cdleme36m  30650  cdlemg17b  30851  cdlemg17h  30857  cdlemk38  31104  cdlemk53b  31145  cdlemkyyN  31151  cdlemk43N  31152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator