MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl113anc Structured version   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  13196  cnhaus  17408  dishaus  17436  ordthauslem  17437  pthaus  17660  txhaus  17669  xkohaus  17675  regr1lem  17761  methaus  18540  metnrmlem3  18881  lt2addrd  24105  xlt2addrd  24114  br8  25369  br4  25371  axpaschlem  25844  btwnxfr  25955  lineext  25975  brsegle  26007  brsegle2  26008  psgnunilem1  27348  n4cyclfrgra  28309  lfl0  29764  lfladd  29765  lflsub  29766  lflmul  29767  lflnegcl  29774  lflvscl  29776  lkrlss  29794  3dimlem3  30159  3dimlem4  30162  3dim3  30167  2llnm3N  30267  2lplnja  30317  4atex  30774  4atex3  30779  trlval4  30886  cdleme7c  30943  cdleme7d  30944  cdleme7ga  30946  cdleme21h  31032  cdleme21i  31033  cdleme21j  31034  cdleme21  31035  cdleme32d  31142  cdleme32f  31144  cdleme35h2  31155  cdleme38m  31161  cdleme40m  31165  cdlemg8  31329  cdlemg11a  31335  cdlemg10a  31338  cdlemg12b  31342  cdlemg12d  31344  cdlemg12f  31346  cdlemg12g  31347  cdlemg15a  31353  cdlemg16  31355  cdlemg16z  31357  cdlemg18a  31376  cdlemg24  31386  cdlemg29  31403  cdlemg33b  31405  cdlemg38  31413  cdlemg39  31414  cdlemg40  31415  cdlemg44b  31430  cdlemj2  31520  cdlemk7  31546  cdlemk12  31548  cdlemk12u  31570  cdlemk32  31595  cdlemk25-3  31602  cdlemk34  31608  cdlemkid3N  31631  cdlemkid4  31632  cdlemk11t  31644  cdlemk53  31655  cdlemk55b  31658  cdleml3N  31676  hdmapln1  32608
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