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  4151  tfisi  4779  fsnunf2  5872  axdc4lem  8269  div32d  9746  div13d  9747  expdivd  11465  pcqmul  13155  pcid  13174  pcneg  13175  pc2dvds  13180  pcz  13182  pcaddlem  13185  pcadd  13186  pcmpt2  13190  pcbc  13197  qexpz  13198  expnprm  13199  spwpr4c  14592  sylow1lem1  15160  lspsneleq  16115  lspsneq  16122  lspfixed  16128  ucncn  18237  ucnextcn  18256  ssblex  18349  prdsxmslem2  18450  voliunlem1  19312  deg1mul3le  19907  deg1pw  19911  fta1blem  19959  bcmono  20929  dchrisum0flblem1  21070  dchrisum0flblem2  21071  pntibndlem1  21151  pntlemr  21164  0wlkon  21412  0pthon  21434  nv1  22014  measun  24360  measvuni  24363  measunl  24365  btwnconn1lem14  25749  segcon2  25754  seglelin  25765  neibastop3  26083  upixp  26123  fdc  26141  eldioph2b  26513  jm2.19lem4  26755  jm2.19  26756  jm2.26a  26763  jm2.26  26765  hbtlem2  26998  fnchoice  27369  stoweidlem42  27460  stoweidlem59  27477  eqlkr3  29217  lkrshp  29221  lfl1dim  29237  lfl1dim2N  29238  eqlkr4  29281  2llnneN  29524  3dim2  29583  4atlem3  29711  4atlem11  29724  4atlem12  29727  pexmidlem4N  30088  lhp2at0nle  30150  lhple  30157  ltrnideq  30290  cdlemd9  30321  cdleme0ex2N  30339  cdleme0moN  30340  cdleme11a  30375  cdleme30a  30493  cdlemefs32sn1aw  30529  cdleme43fsv1snlem  30535  cdlemefs31fv1  30539  cdlemefs45eN  30546  cdleme41sn3a  30548  cdleme35h  30571  cdleme36a  30575  cdleme40m  30582  cdleme40n  30583  cdleme41sn3aw  30589  cdleme42h  30597  cdleme42k  30599  cdleme42mN  30602  cdleme43cN  30606  cdleme17d3  30611  cdleme48fvg  30615  cdlemeg47rv2  30625  cdlemeg46c  30628  cdlemeg46sfg  30635  cdlemeg46rjgN  30637  cdlemeg46rgv  30643  cdlemeg46req  30644  cdlemeg46gfv  30645  cdlemeg46gfre  30647  cdlemeg49lebilem  30654  cdleme50trn2  30666  cdlemg2kq  30717  cdlemb3  30721  cdlemg4f  30730  cdlemg9a  30747  cdlemg9b  30748  cdlemg9  30749  cdlemg11aq  30753  cdlemg12a  30758  cdlemg12b  30759  cdlemg12c  30760  cdlemg12d  30761  cdlemg12f  30763  cdlemg12g  30764  cdlemg12  30765  cdlemg13a  30766  cdlemg16  30772  cdlemg17e  30780  cdlemg17f  30781  cdlemg17g  30782  cdlemg17ir  30785  cdlemg17  30792  cdlemg18b  30794  cdlemg18c  30795  cdlemg33e  30825  trlcoabs2N  30837  trlcocnvat  30839  trlcolem  30841  trlco  30842  cdlemg44  30848  cdlemg47  30851  ltrncom  30853  tendococl  30887  tendoplcl  30896  tendoplcom  30897  tendoplass  30898  tendodi1  30899  tendodi2  30900  tendo0pl  30906  tendoipl  30912  cdlemh1  30930  cdlemi2  30934  tendo0mul  30941  tendo0mulr  30942  cdlemk2  30947  cdlemk3  30948  cdlemk4  30949  cdlemk6  30952  cdlemk8  30953  cdlemk12  30965  cdlemkole  30968  cdlemk14  30969  cdlemk15  30970  cdlemk5u  30976  cdlemk6u  30977  cdlemk12u  30987  cdlemkfid1N  31036  cdlemk19x  31058  cdlemk48  31065  cdlemk53a  31070  cdlemk56  31086  cdleml2N  31092  cdleml3N  31093  cdleml6  31096  cdleml7  31097  dva1dim  31100  dia2dimlem4  31183  dvhlveclem  31224  doca2N  31242  djajN  31253  cdlemn2a  31312  cdlemn3  31313  dihordlem6  31329  dihord5apre  31378  dihglbcpreN  31416  dihmeetcN  31418  dihmeetbN  31419  dihmeetlem10N  31432  dihmeetlem12N  31434  dihmeetlem15N  31437  dihmeetALTN  31443  dih1dimatlem0  31444  dihjatcclem3  31536  dihjatcclem4  31537  mapdpglem22  31809  hdmap14lem1a  31985
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