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  12802  brbtwn2  24605  3atlem4  30297  3atlem6  30299  llnexchb2  30680  osumcllem9N  30775  cdlemd4  31012  cdleme26fALTN  31173  cdleme26f  31174  cdleme36m  31272  cdlemg17b  31473  cdlemg17h  31479  cdlemk38  31726  cdlemk53b  31767  cdlemkyyN  31773  cdlemk43N  31774
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