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

Theorem syl113anc 1196
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 1134 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1184 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl123anc  1201  syl213anc  1203  pythagtriplem18  13133  cnhaus  17340  dishaus  17368  ordthauslem  17369  pthaus  17591  txhaus  17600  xkohaus  17606  regr1lem  17692  methaus  18440  metnrmlem3  18762  lt2addrd  23956  xlt2addrd  23960  br8  25137  br4  25139  axpaschlem  25593  btwnxfr  25704  lineext  25724  brsegle  25756  brsegle2  25757  psgnunilem1  27085  n4cyclfrgra  27771  lfl0  29180  lfladd  29181  lflsub  29182  lflmul  29183  lflnegcl  29190  lflvscl  29192  lkrlss  29210  3dimlem3  29575  3dimlem4  29578  3dim3  29583  2llnm3N  29683  2lplnja  29733  4atex  30190  4atex3  30195  trlval4  30302  cdleme7c  30359  cdleme7d  30360  cdleme7ga  30362  cdleme21h  30448  cdleme21i  30449  cdleme21j  30450  cdleme21  30451  cdleme32d  30558  cdleme32f  30560  cdleme35h2  30571  cdleme38m  30577  cdleme40m  30581  cdlemg8  30745  cdlemg11a  30751  cdlemg10a  30754  cdlemg12b  30758  cdlemg12d  30760  cdlemg12f  30762  cdlemg12g  30763  cdlemg15a  30769  cdlemg16  30771  cdlemg16z  30773  cdlemg18a  30792  cdlemg24  30802  cdlemg29  30819  cdlemg33b  30821  cdlemg38  30829  cdlemg39  30830  cdlemg40  30831  cdlemg44b  30846  cdlemj2  30936  cdlemk7  30962  cdlemk12  30964  cdlemk12u  30986  cdlemk32  31011  cdlemk25-3  31018  cdlemk34  31024  cdlemkid3N  31047  cdlemkid4  31048  cdlemk11t  31060  cdlemk53  31071  cdlemk55b  31074  cdleml3N  31092  hdmapln1  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator