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

Theorem syl311anc 1199
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 1135 . 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 1185 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  syl312anc  1206  syl321anc  1207  syl313anc  1209  syl331anc  1210  pythagtrip  13239  nmolb2d  18783  nmoleub  18796  cvlcvr1  30235  4atlem12b  30506  dalawlem10  30775  dalawlem13  30778  dalawlem15  30780  osumcllem11N  30861  lhp2atne  30929  lhp2at0ne  30931  cdlemd  31102  ltrneq3  31103  cdleme7d  31141  cdlemeg49le  31406  cdleme  31455  cdlemg1a  31465  ltrniotavalbN  31479  cdlemg44  31628  cdlemk19  31764  cdlemk27-3  31802  cdlemk33N  31804  cdlemk34  31805  cdlemk49  31846  cdlemk53a  31850  cdlemk19u  31865  cdlemk56w  31868  dia2dimlem4  31963  dih1dimatlem0  32224
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator