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

Theorem syl331anc 1210
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 1135 . 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 1199 1  |-  ( ph  ->  rh )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  syl332anc  1216  syl333anc  1217  qredeu  13109  brbtwn2  25846  3atlem4  30345  3atlem6  30347  llnexchb2  30728  osumcllem9N  30823  cdlemd4  31060  cdleme26fALTN  31221  cdleme26f  31222  cdleme36m  31320  cdlemg17b  31521  cdlemg17h  31527  cdlemk38  31774  cdlemk53b  31815  cdlemkyyN  31821  cdlemk43N  31822
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator