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

Theorem syl321anc 1204
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 518 . 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 1196 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl322anc  1210  cxple2ad  20088  chordthmlem3  20147  islimrs4  25685  4noncolr2  30265  4noncolr1  30266  3atlem5  30298  2lplnj  30431  llnmod2i2  30674  dalawlem11  30692  dalawlem12  30693  cdleme43dN  31303  cdleme4gfv  31318  cdlemeg46nlpq  31328  cdlemg17bq  31484  cdlemg31b0N  31505  cdlemg31b0a  31506  cdlemg31c  31510  cdlemg39  31527  cdlemk47  31760
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