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

Theorem syl113anc 1279
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 1187 . 2  |-  ( ph  ->  ( th  /\  ta  /\  et ) )
7 syl113anc.6 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta  /\  et ) )  ->  ze )
81, 2, 6, 7syl3anc 1267 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 984
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 189  df-an 373  df-3an 986
This theorem is referenced by:  syl123anc  1284  syl213anc  1286  pythagtriplem18  14775  initoeu2  15904  psgnunilem1  17127  mulmarep1gsum1  19591  mulmarep1gsum2  19592  smadiadetlem4  19687  cramerimplem2  19702  cramerlem2  19706  cramer  19709  cnhaus  20363  dishaus  20391  ordthauslem  20392  pthaus  20646  txhaus  20655  xkohaus  20661  regr1lem  20747  methaus  21528  metnrmlem3  21871  metnrmlem3OLD  21886  f1otrge  24895  axpaschlem  24963  n4cyclfrgra  25739  br8d  28211  lt2addrd  28319  xlt2addrd  28331  br8  30389  br4  30391  btwnxfr  30816  lineext  30836  brsegle  30868  brsegle2  30869  lfl0  32625  lfladd  32626  lflsub  32627  lflmul  32628  lflnegcl  32635  lflvscl  32637  lkrlss  32655  3dimlem3  33020  3dimlem4  33023  3dim3  33028  2llnm3N  33128  2lplnja  33178  4atex  33635  4atex3  33640  trlval4  33748  cdleme7c  33805  cdleme7d  33806  cdleme7ga  33808  cdleme21h  33895  cdleme21i  33896  cdleme21j  33897  cdleme21  33898  cdleme32d  34005  cdleme32f  34007  cdleme35h2  34018  cdleme38m  34024  cdleme40m  34028  cdlemg8  34192  cdlemg11a  34198  cdlemg10a  34201  cdlemg12b  34205  cdlemg12d  34207  cdlemg12f  34209  cdlemg12g  34210  cdlemg15a  34216  cdlemg16  34218  cdlemg16z  34220  cdlemg18a  34239  cdlemg24  34249  cdlemg29  34266  cdlemg33b  34268  cdlemg38  34276  cdlemg39  34277  cdlemg40  34278  cdlemg44b  34293  cdlemj2  34383  cdlemk7  34409  cdlemk12  34411  cdlemk12u  34433  cdlemk32  34458  cdlemk25-3  34465  cdlemk34  34471  cdlemkid3N  34494  cdlemkid4  34495  cdlemk11t  34507  cdlemk53  34518  cdlemk55b  34521  cdleml3N  34539  hdmapln1  35471
  Copyright terms: Public domain W3C validator