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

Theorem syl311anc 1232
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 )
syl311anc.6  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  et )  ->  ze )
Assertion
Ref Expression
syl311anc  |-  ( ph  ->  ze )

Proof of Theorem syl311anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1168 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 syl311anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  et )  ->  ze )
84, 5, 6, 7syl3anc 1218 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  syl312anc  1239  syl321anc  1240  syl313anc  1242  syl331anc  1243  pythagtrip  13899  nmolb2d  20295  nmoleub  20308  clwwisshclwwlem  30467  cvlcvr1  32981  4atlem12b  33252  dalawlem10  33521  dalawlem13  33524  dalawlem15  33526  osumcllem11N  33607  lhp2atne  33675  lhp2at0ne  33677  cdlemd  33848  ltrneq3  33849  cdleme7d  33887  cdlemeg49le  34152  cdleme  34201  cdlemg1a  34211  ltrniotavalbN  34225  cdlemg44  34374  cdlemk19  34510  cdlemk27-3  34548  cdlemk33N  34550  cdlemk34  34551  cdlemk49  34592  cdlemk53a  34596  cdlemk19u  34611  cdlemk56w  34614  dia2dimlem4  34709  dih1dimatlem0  34970
  Copyright terms: Public domain W3C validator