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

Theorem syl113anc 1194
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 1132 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1182 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl123anc  1199  syl213anc  1201  pythagtriplem18  12901  cnhaus  17098  dishaus  17126  ordthauslem  17127  pthaus  17348  txhaus  17357  xkohaus  17363  regr1lem  17446  methaus  18082  metnrmlem3  18381  br8  24184  br4  24186  axpaschlem  24640  btwnxfr  24751  lineext  24771  brsegle  24803  brsegle2  24804  psgnunilem1  27519  n4cyclfrgra  28440  lfl0  29877  lfladd  29878  lflsub  29879  lflmul  29880  lflnegcl  29887  lflvscl  29889  lkrlss  29907  3dimlem3  30272  3dimlem4  30275  3dim3  30280  2llnm3N  30380  2lplnja  30430  4atex  30887  4atex3  30892  trlval4  30999  cdleme7c  31056  cdleme7d  31057  cdleme7ga  31059  cdleme21h  31145  cdleme21i  31146  cdleme21j  31147  cdleme21  31148  cdleme32d  31255  cdleme32f  31257  cdleme35h2  31268  cdleme38m  31274  cdleme40m  31278  cdlemg8  31442  cdlemg11a  31448  cdlemg10a  31451  cdlemg12b  31455  cdlemg12d  31457  cdlemg12f  31459  cdlemg12g  31460  cdlemg15a  31466  cdlemg16  31468  cdlemg16z  31470  cdlemg18a  31489  cdlemg24  31499  cdlemg29  31516  cdlemg33b  31518  cdlemg38  31526  cdlemg39  31527  cdlemg40  31528  cdlemg44b  31543  cdlemj2  31633  cdlemk7  31659  cdlemk12  31661  cdlemk12u  31683  cdlemk32  31708  cdlemk25-3  31715  cdlemk34  31721  cdlemkid3N  31744  cdlemkid4  31745  cdlemk11t  31757  cdlemk53  31768  cdlemk55b  31771  cdleml3N  31789  hdmapln1  32721
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator