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  14367  initoeu2  15421  psgnunilem1  16644  mulmarep1gsum1  19201  mulmarep1gsum2  19202  smadiadetlem4  19297  cramerimplem2  19312  cramerlem2  19316  cramer  19319  cnhaus  19981  dishaus  20009  ordthauslem  20010  pthaus  20264  txhaus  20273  xkohaus  20279  regr1lem  20365  methaus  21148  metnrmlem3  21490  f1otrge  24301  axpaschlem  24369  n4cyclfrgra  25144  br8d  27601  lt2addrd  27713  xlt2addrd  27728  br8  29360  br4  29362  btwnxfr  29868  lineext  29888  brsegle  29920  brsegle2  29921  lfl0  34891  lfladd  34892  lflsub  34893  lflmul  34894  lflnegcl  34901  lflvscl  34903  lkrlss  34921  3dimlem3  35286  3dimlem4  35289  3dim3  35294  2llnm3N  35394  2lplnja  35444  4atex  35901  4atex3  35906  trlval4  36014  cdleme7c  36071  cdleme7d  36072  cdleme7ga  36074  cdleme21h  36161  cdleme21i  36162  cdleme21j  36163  cdleme21  36164  cdleme32d  36271  cdleme32f  36273  cdleme35h2  36284  cdleme38m  36290  cdleme40m  36294  cdlemg8  36458  cdlemg11a  36464  cdlemg10a  36467  cdlemg12b  36471  cdlemg12d  36473  cdlemg12f  36475  cdlemg12g  36476  cdlemg15a  36482  cdlemg16  36484  cdlemg16z  36486  cdlemg18a  36505  cdlemg24  36515  cdlemg29  36532  cdlemg33b  36534  cdlemg38  36542  cdlemg39  36543  cdlemg40  36544  cdlemg44b  36559  cdlemj2  36649  cdlemk7  36675  cdlemk12  36677  cdlemk12u  36699  cdlemk32  36724  cdlemk25-3  36731  cdlemk34  36737  cdlemkid3N  36760  cdlemkid4  36761  cdlemk11t  36773  cdlemk53  36784  cdlemk55b  36787  cdleml3N  36805  hdmapln1  37737
  Copyright terms: Public domain W3C validator