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

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

Proof of Theorem syl113anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
63, 4, 53jca 1176 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1228 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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:  syl123anc  1245  syl213anc  1247  pythagtriplem18  14211  psgnunilem1  16314  mulmarep1gsum1  18842  mulmarep1gsum2  18843  smadiadetlem4  18938  cramerimplem2  18953  cramerlem2  18957  cramer  18960  cnhaus  19621  dishaus  19649  ordthauslem  19650  pthaus  19874  txhaus  19883  xkohaus  19889  regr1lem  19975  methaus  20758  metnrmlem3  21100  axpaschlem  23919  n4cyclfrgra  24694  br8d  27136  lt2addrd  27231  xlt2addrd  27246  br8  28762  br4  28764  btwnxfr  29283  lineext  29303  brsegle  29335  brsegle2  29336  lfl0  33862  lfladd  33863  lflsub  33864  lflmul  33865  lflnegcl  33872  lflvscl  33874  lkrlss  33892  3dimlem3  34257  3dimlem4  34260  3dim3  34265  2llnm3N  34365  2lplnja  34415  4atex  34872  4atex3  34877  trlval4  34984  cdleme7c  35041  cdleme7d  35042  cdleme7ga  35044  cdleme21h  35130  cdleme21i  35131  cdleme21j  35132  cdleme21  35133  cdleme32d  35240  cdleme32f  35242  cdleme35h2  35253  cdleme38m  35259  cdleme40m  35263  cdlemg8  35427  cdlemg11a  35433  cdlemg10a  35436  cdlemg12b  35440  cdlemg12d  35442  cdlemg12f  35444  cdlemg12g  35445  cdlemg15a  35451  cdlemg16  35453  cdlemg16z  35455  cdlemg18a  35474  cdlemg24  35484  cdlemg29  35501  cdlemg33b  35503  cdlemg38  35511  cdlemg39  35512  cdlemg40  35513  cdlemg44b  35528  cdlemj2  35618  cdlemk7  35644  cdlemk12  35646  cdlemk12u  35668  cdlemk32  35693  cdlemk25-3  35700  cdlemk34  35706  cdlemkid3N  35729  cdlemkid4  35730  cdlemk11t  35742  cdlemk53  35753  cdlemk55b  35756  cdleml3N  35774  hdmapln1  36706
  Copyright terms: Public domain W3C validator