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

Theorem syl121anc 1189
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 )
syl121anc.5  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl121anc  |-  ( ph  ->  et )

Proof of Theorem syl121anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
42, 3jca 519 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1184 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl122anc  1193  disjxiun  4150  tfisi  4778  fsnunf2  5871  axdc4lem  8268  div32d  9745  div13d  9746  expdivd  11464  pcqmul  13154  pcid  13173  pcneg  13174  pc2dvds  13179  pcz  13181  pcaddlem  13184  pcadd  13185  pcmpt2  13189  pcbc  13196  qexpz  13197  expnprm  13198  spwpr4c  14591  sylow1lem1  15159  lspsneleq  16114  lspsneq  16121  lspfixed  16127  ucncn  18236  ucnextcn  18255  ssblex  18348  prdsxmslem2  18449  voliunlem1  19311  deg1mul3le  19906  deg1pw  19910  fta1blem  19958  bcmono  20928  dchrisum0flblem1  21069  dchrisum0flblem2  21070  pntibndlem1  21150  pntlemr  21163  0wlkon  21411  0pthon  21433  nv1  22013  measun  24359  measvuni  24362  measunl  24364  btwnconn1lem14  25748  segcon2  25753  seglelin  25764  neibastop3  26082  upixp  26122  fdc  26140  eldioph2b  26512  jm2.19lem4  26754  jm2.19  26755  jm2.26a  26762  jm2.26  26764  hbtlem2  26997  fnchoice  27368  stoweidlem42  27459  stoweidlem59  27476  eqlkr3  29216  lkrshp  29220  lfl1dim  29236  lfl1dim2N  29237  eqlkr4  29280  2llnneN  29523  3dim2  29582  4atlem3  29710  4atlem11  29723  4atlem12  29726  pexmidlem4N  30087  lhp2at0nle  30149  lhple  30156  ltrnideq  30289  cdlemd9  30320  cdleme0ex2N  30338  cdleme0moN  30339  cdleme11a  30374  cdleme30a  30492  cdlemefs32sn1aw  30528  cdleme43fsv1snlem  30534  cdlemefs31fv1  30538  cdlemefs45eN  30545  cdleme41sn3a  30547  cdleme35h  30570  cdleme36a  30574  cdleme40m  30581  cdleme40n  30582  cdleme41sn3aw  30588  cdleme42h  30596  cdleme42k  30598  cdleme42mN  30601  cdleme43cN  30605  cdleme17d3  30610  cdleme48fvg  30614  cdlemeg47rv2  30624  cdlemeg46c  30627  cdlemeg46sfg  30634  cdlemeg46rjgN  30636  cdlemeg46rgv  30642  cdlemeg46req  30643  cdlemeg46gfv  30644  cdlemeg46gfre  30646  cdlemeg49lebilem  30653  cdleme50trn2  30665  cdlemg2kq  30716  cdlemb3  30720  cdlemg4f  30729  cdlemg9a  30746  cdlemg9b  30747  cdlemg9  30748  cdlemg11aq  30752  cdlemg12a  30757  cdlemg12b  30758  cdlemg12c  30759  cdlemg12d  30760  cdlemg12f  30762  cdlemg12g  30763  cdlemg12  30764  cdlemg13a  30765  cdlemg16  30771  cdlemg17e  30779  cdlemg17f  30780  cdlemg17g  30781  cdlemg17ir  30784  cdlemg17  30791  cdlemg18b  30793  cdlemg18c  30794  cdlemg33e  30824  trlcoabs2N  30836  trlcocnvat  30838  trlcolem  30840  trlco  30841  cdlemg44  30847  cdlemg47  30850  ltrncom  30852  tendococl  30886  tendoplcl  30895  tendoplcom  30896  tendoplass  30897  tendodi1  30898  tendodi2  30899  tendo0pl  30905  tendoipl  30911  cdlemh1  30929  cdlemi2  30933  tendo0mul  30940  tendo0mulr  30941  cdlemk2  30946  cdlemk3  30947  cdlemk4  30948  cdlemk6  30951  cdlemk8  30952  cdlemk12  30964  cdlemkole  30967  cdlemk14  30968  cdlemk15  30969  cdlemk5u  30975  cdlemk6u  30976  cdlemk12u  30986  cdlemkfid1N  31035  cdlemk19x  31057  cdlemk48  31064  cdlemk53a  31069  cdlemk56  31085  cdleml2N  31091  cdleml3N  31092  cdleml6  31095  cdleml7  31096  dva1dim  31099  dia2dimlem4  31182  dvhlveclem  31223  doca2N  31241  djajN  31252  cdlemn2a  31311  cdlemn3  31312  dihordlem6  31328  dihord5apre  31377  dihglbcpreN  31415  dihmeetcN  31417  dihmeetbN  31418  dihmeetlem10N  31431  dihmeetlem12N  31433  dihmeetlem15N  31436  dihmeetALTN  31442  dih1dimatlem0  31443  dihjatcclem3  31535  dihjatcclem4  31536  mapdpglem22  31808  hdmap14lem1a  31984
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