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

Theorem syl113anc 1230
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 1168 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 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:  syl123anc  1235  syl213anc  1237  pythagtriplem18  13891  psgnunilem1  15990  mulmarep1gsum1  18359  mulmarep1gsum2  18360  smadiadetlem4  18450  cramerimplem2  18465  cramerlem2  18469  cramer  18472  cnhaus  18933  dishaus  18961  ordthauslem  18962  pthaus  19186  txhaus  19195  xkohaus  19201  regr1lem  19287  methaus  20070  metnrmlem3  20412  axpaschlem  23137  br8d  25893  lt2addrd  25987  xlt2addrd  26002  br8  27517  br4  27519  btwnxfr  28038  lineext  28058  brsegle  28090  brsegle2  28091  n4cyclfrgra  30563  lfl0  32550  lfladd  32551  lflsub  32552  lflmul  32553  lflnegcl  32560  lflvscl  32562  lkrlss  32580  3dimlem3  32945  3dimlem4  32948  3dim3  32953  2llnm3N  33053  2lplnja  33103  4atex  33560  4atex3  33565  trlval4  33672  cdleme7c  33729  cdleme7d  33730  cdleme7ga  33732  cdleme21h  33818  cdleme21i  33819  cdleme21j  33820  cdleme21  33821  cdleme32d  33928  cdleme32f  33930  cdleme35h2  33941  cdleme38m  33947  cdleme40m  33951  cdlemg8  34115  cdlemg11a  34121  cdlemg10a  34124  cdlemg12b  34128  cdlemg12d  34130  cdlemg12f  34132  cdlemg12g  34133  cdlemg15a  34139  cdlemg16  34141  cdlemg16z  34143  cdlemg18a  34162  cdlemg24  34172  cdlemg29  34189  cdlemg33b  34191  cdlemg38  34199  cdlemg39  34200  cdlemg40  34201  cdlemg44b  34216  cdlemj2  34306  cdlemk7  34332  cdlemk12  34334  cdlemk12u  34356  cdlemk32  34381  cdlemk25-3  34388  cdlemk34  34394  cdlemkid3N  34417  cdlemkid4  34418  cdlemk11t  34430  cdlemk53  34441  cdlemk55b  34444  cdleml3N  34462  hdmapln1  35394
  Copyright terms: Public domain W3C validator