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

Theorem syl113anc 1276
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 1185 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1264 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  syl123anc  1281  syl213anc  1283  pythagtriplem18  14769  initoeu2  15898  psgnunilem1  17121  mulmarep1gsum1  19584  mulmarep1gsum2  19585  smadiadetlem4  19680  cramerimplem2  19695  cramerlem2  19699  cramer  19702  cnhaus  20356  dishaus  20384  ordthauslem  20385  pthaus  20639  txhaus  20648  xkohaus  20654  regr1lem  20740  methaus  21521  metnrmlem3  21864  metnrmlem3OLD  21879  f1otrge  24888  axpaschlem  24956  n4cyclfrgra  25731  br8d  28207  lt2addrd  28319  xlt2addrd  28331  br8  30390  br4  30392  btwnxfr  30815  lineext  30835  brsegle  30867  brsegle2  30868  lfl0  32549  lfladd  32550  lflsub  32551  lflmul  32552  lflnegcl  32559  lflvscl  32561  lkrlss  32579  3dimlem3  32944  3dimlem4  32947  3dim3  32952  2llnm3N  33052  2lplnja  33102  4atex  33559  4atex3  33564  trlval4  33672  cdleme7c  33729  cdleme7d  33730  cdleme7ga  33732  cdleme21h  33819  cdleme21i  33820  cdleme21j  33821  cdleme21  33822  cdleme32d  33929  cdleme32f  33931  cdleme35h2  33942  cdleme38m  33948  cdleme40m  33952  cdlemg8  34116  cdlemg11a  34122  cdlemg10a  34125  cdlemg12b  34129  cdlemg12d  34131  cdlemg12f  34133  cdlemg12g  34134  cdlemg15a  34140  cdlemg16  34142  cdlemg16z  34144  cdlemg18a  34163  cdlemg24  34173  cdlemg29  34190  cdlemg33b  34192  cdlemg38  34200  cdlemg39  34201  cdlemg40  34202  cdlemg44b  34217  cdlemj2  34307  cdlemk7  34333  cdlemk12  34335  cdlemk12u  34357  cdlemk32  34382  cdlemk25-3  34389  cdlemk34  34395  cdlemkid3N  34418  cdlemkid4  34419  cdlemk11t  34431  cdlemk53  34442  cdlemk55b  34445  cdleml3N  34463  hdmapln1  35395
  Copyright terms: Public domain W3C validator