MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl321anc Structured version   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  20608  chordthmlem3  20667  4noncolr2  30188  4noncolr1  30189  3atlem5  30221  2lplnj  30354  llnmod2i2  30597  dalawlem11  30615  dalawlem12  30616  cdleme43dN  31226  cdleme4gfv  31241  cdlemeg46nlpq  31251  cdlemg17bq  31407  cdlemg31b0N  31428  cdlemg31b0a  31429  cdlemg31c  31433  cdlemg39  31450  cdlemk47  31683
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