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

Theorem syl113anc 1223
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 1161 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1211 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958
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 960
This theorem is referenced by:  syl123anc  1228  syl213anc  1230  pythagtriplem18  13881  psgnunilem1  15978  mulmarep1gsum1  18225  mulmarep1gsum2  18226  smadiadetlem4  18316  cramerimplem2  18331  cramerlem2  18335  cramer  18338  cnhaus  18799  dishaus  18827  ordthauslem  18828  pthaus  19052  txhaus  19061  xkohaus  19067  regr1lem  19153  methaus  19936  metnrmlem3  20278  axpaschlem  23008  br8d  25765  lt2addrd  25860  xlt2addrd  25875  br8  27412  br4  27414  btwnxfr  27933  lineext  27953  brsegle  27985  brsegle2  27986  n4cyclfrgra  30453  lfl0  32280  lfladd  32281  lflsub  32282  lflmul  32283  lflnegcl  32290  lflvscl  32292  lkrlss  32310  3dimlem3  32675  3dimlem4  32678  3dim3  32683  2llnm3N  32783  2lplnja  32833  4atex  33290  4atex3  33295  trlval4  33402  cdleme7c  33459  cdleme7d  33460  cdleme7ga  33462  cdleme21h  33548  cdleme21i  33549  cdleme21j  33550  cdleme21  33551  cdleme32d  33658  cdleme32f  33660  cdleme35h2  33671  cdleme38m  33677  cdleme40m  33681  cdlemg8  33845  cdlemg11a  33851  cdlemg10a  33854  cdlemg12b  33858  cdlemg12d  33860  cdlemg12f  33862  cdlemg12g  33863  cdlemg15a  33869  cdlemg16  33871  cdlemg16z  33873  cdlemg18a  33892  cdlemg24  33902  cdlemg29  33919  cdlemg33b  33921  cdlemg38  33929  cdlemg39  33930  cdlemg40  33931  cdlemg44b  33946  cdlemj2  34036  cdlemk7  34062  cdlemk12  34064  cdlemk12u  34086  cdlemk32  34111  cdlemk25-3  34118  cdlemk34  34124  cdlemkid3N  34147  cdlemkid4  34148  cdlemk11t  34160  cdlemk53  34171  cdlemk55b  34174  cdleml3N  34192  hdmapln1  35124
  Copyright terms: Public domain W3C validator