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

Theorem syl321anc 1206
Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-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 )
syl321anc.7  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ze )  ->  si )
Assertion
Ref Expression
syl321anc  |-  ( ph  ->  si )

Proof of Theorem syl321anc
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 )
64, 5jca 519 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 sylXanc.6 . 2  |-  ( ph  ->  ze )
8 syl321anc.7 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ze )  ->  si )
91, 2, 3, 6, 7, 8syl311anc 1198 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl322anc  1212  cxple2ad  20483  chordthmlem3  20542  4noncolr2  29568  4noncolr1  29569  3atlem5  29601  2lplnj  29734  llnmod2i2  29977  dalawlem11  29995  dalawlem12  29996  cdleme43dN  30606  cdleme4gfv  30621  cdlemeg46nlpq  30631  cdlemg17bq  30787  cdlemg31b0N  30808  cdlemg31b0a  30809  cdlemg31c  30813  cdlemg39  30830  cdlemk47  31063
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator