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

Theorem syl121anc 1190
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 520 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1185 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  syl122anc  1194  disjxiun  4212  tfisi  4841  fsnunf2  5935  axdc4lem  8340  div32d  9818  div13d  9819  expdivd  11542  pcqmul  13232  pcid  13251  pcneg  13252  pc2dvds  13257  pcz  13259  pcaddlem  13262  pcadd  13263  pcmpt2  13267  pcbc  13274  qexpz  13275  expnprm  13276  spwpr4c  14669  sylow1lem1  15237  lspsneleq  16192  lspsneq  16199  lspfixed  16205  ucncn  18320  ucnextcn  18339  ssblex  18463  prdsxmslem2  18564  voliunlem1  19449  deg1mul3le  20044  deg1pw  20048  fta1blem  20096  bcmono  21066  dchrisum0flblem1  21207  dchrisum0flblem2  21208  pntibndlem1  21288  pntlemr  21301  0wlkon  21552  0pthon  21584  nv1  22170  measun  24570  measvuni  24573  measunl  24575  btwnconn1lem14  26039  segcon2  26044  seglelin  26055  neibastop3  26405  upixp  26445  fdc  26463  eldioph2b  26835  jm2.19lem4  27077  jm2.19  27078  jm2.26a  27085  jm2.26  27087  hbtlem2  27319  fnchoice  27690  stoweidlem42  27781  stoweidlem59  27798  eqlkr3  29973  lkrshp  29977  lfl1dim  29993  lfl1dim2N  29994  eqlkr4  30037  2llnneN  30280  3dim2  30339  4atlem3  30467  4atlem11  30480  4atlem12  30483  pexmidlem4N  30844  lhp2at0nle  30906  lhple  30913  ltrnideq  31046  cdlemd9  31077  cdleme0ex2N  31095  cdleme0moN  31096  cdleme11a  31131  cdleme30a  31249  cdlemefs32sn1aw  31285  cdleme43fsv1snlem  31291  cdlemefs31fv1  31295  cdlemefs45eN  31302  cdleme41sn3a  31304  cdleme35h  31327  cdleme36a  31331  cdleme40m  31338  cdleme40n  31339  cdleme41sn3aw  31345  cdleme42h  31353  cdleme42k  31355  cdleme42mN  31358  cdleme43cN  31362  cdleme17d3  31367  cdleme48fvg  31371  cdlemeg47rv2  31381  cdlemeg46c  31384  cdlemeg46sfg  31391  cdlemeg46rjgN  31393  cdlemeg46rgv  31399  cdlemeg46req  31400  cdlemeg46gfv  31401  cdlemeg46gfre  31403  cdlemeg49lebilem  31410  cdleme50trn2  31422  cdlemg2kq  31473  cdlemb3  31477  cdlemg4f  31486  cdlemg9a  31503  cdlemg9b  31504  cdlemg9  31505  cdlemg11aq  31509  cdlemg12a  31514  cdlemg12b  31515  cdlemg12c  31516  cdlemg12d  31517  cdlemg12f  31519  cdlemg12g  31520  cdlemg12  31521  cdlemg13a  31522  cdlemg16  31528  cdlemg17e  31536  cdlemg17f  31537  cdlemg17g  31538  cdlemg17ir  31541  cdlemg17  31548  cdlemg18b  31550  cdlemg18c  31551  cdlemg33e  31581  trlcoabs2N  31593  trlcocnvat  31595  trlcolem  31597  trlco  31598  cdlemg44  31604  cdlemg47  31607  ltrncom  31609  tendococl  31643  tendoplcl  31652  tendoplcom  31653  tendoplass  31654  tendodi1  31655  tendodi2  31656  tendo0pl  31662  tendoipl  31668  cdlemh1  31686  cdlemi2  31690  tendo0mul  31697  tendo0mulr  31698  cdlemk2  31703  cdlemk3  31704  cdlemk4  31705  cdlemk6  31708  cdlemk8  31709  cdlemk12  31721  cdlemkole  31724  cdlemk14  31725  cdlemk15  31726  cdlemk5u  31732  cdlemk6u  31733  cdlemk12u  31743  cdlemkfid1N  31792  cdlemk19x  31814  cdlemk48  31821  cdlemk53a  31826  cdlemk56  31842  cdleml2N  31848  cdleml3N  31849  cdleml6  31852  cdleml7  31853  dva1dim  31856  dia2dimlem4  31939  dvhlveclem  31980  doca2N  31998  djajN  32009  cdlemn2a  32068  cdlemn3  32069  dihordlem6  32085  dihord5apre  32134  dihglbcpreN  32172  dihmeetcN  32174  dihmeetbN  32175  dihmeetlem10N  32188  dihmeetlem12N  32190  dihmeetlem15N  32193  dihmeetALTN  32199  dih1dimatlem0  32200  dihjatcclem3  32292  dihjatcclem4  32293  mapdpglem22  32565  hdmap14lem1a  32741
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator