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

Theorem syl321anc 1250
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 532 . 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 1242 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  syl322anc  1256  cxple2ad  22931  chordthmlem3  22990  lincext3  32355  4noncolr2  34467  4noncolr1  34468  3atlem5  34500  2lplnj  34633  llnmod2i2  34876  dalawlem11  34894  dalawlem12  34895  cdleme43dN  35505  cdleme4gfv  35520  cdlemeg46nlpq  35530  cdlemg17bq  35686  cdlemg31b0N  35707  cdlemg31b0a  35708  cdlemg31c  35712  cdlemg39  35729  cdlemk47  35962
  Copyright terms: Public domain W3C validator