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

Theorem syl121anc 1187
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 518 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1182 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl122anc  1191  disjxiun  4036  tfisi  4665  fsnunf2  5735  axdc4lem  8097  div32d  9575  div13d  9576  expdivd  11275  pcqmul  12922  pcid  12941  pcneg  12942  pc2dvds  12947  pcz  12949  pcaddlem  12952  pcadd  12953  pcmpt2  12957  pcbc  12964  qexpz  12965  expnprm  12966  spwpr4c  14357  sylow1lem1  14925  lmodvsnegOLD  15684  lspsneleq  15884  lspsneq  15891  lspfixed  15897  ssblex  17990  prdsxmslem2  18091  voliunlem1  18923  deg1mul3le  19518  deg1pw  19522  fta1blem  19570  bcmono  20532  dchrisum0flblem1  20673  dchrisum0flblem2  20674  pntibndlem1  20754  pntlemr  20767  nv1  21258  measxun  23554  btwnconn1lem14  24795  segcon2  24800  seglelin  24811  toplat  25393  islimrs4  25685  idmon  25920  cmp2morpcats  26064  cmpmorass  26069  cmpidmor2  26072  cmpidmor3  26073  neibastop3  26414  upixp  26506  fdc  26558  eldioph2b  26945  jm2.19lem4  27188  jm2.19  27189  jm2.26a  27196  jm2.26  27198  hbtlem2  27431  eqlkr3  29913  lkrshp  29917  lfl1dim  29933  lfl1dim2N  29934  eqlkr4  29977  2llnneN  30220  3dim2  30279  4atlem3  30407  4atlem11  30420  4atlem12  30423  pexmidlem4N  30784  lhp2at0nle  30846  lhple  30853  ltrnideq  30986  cdlemd9  31017  cdleme0ex2N  31035  cdleme0moN  31036  cdleme11a  31071  cdleme30a  31189  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdlemefs31fv1  31235  cdlemefs45eN  31242  cdleme41sn3a  31244  cdleme35h  31267  cdleme36a  31271  cdleme40m  31278  cdleme40n  31279  cdleme41sn3aw  31285  cdleme42h  31293  cdleme42k  31295  cdleme42mN  31298  cdleme43cN  31302  cdleme17d3  31307  cdleme48fvg  31311  cdlemeg47rv2  31321  cdlemeg46c  31324  cdlemeg46sfg  31331  cdlemeg46rjgN  31333  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdlemeg46gfre  31343  cdlemeg49lebilem  31350  cdleme50trn2  31362  cdlemg2kq  31413  cdlemb3  31417  cdlemg4f  31426  cdlemg9a  31443  cdlemg9b  31444  cdlemg9  31445  cdlemg11aq  31449  cdlemg12a  31454  cdlemg12b  31455  cdlemg12c  31456  cdlemg12d  31457  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg16  31468  cdlemg17e  31476  cdlemg17f  31477  cdlemg17g  31478  cdlemg17ir  31481  cdlemg17  31488  cdlemg18b  31490  cdlemg18c  31491  cdlemg33e  31521  trlcoabs2N  31533  trlcocnvat  31535  trlcolem  31537  trlco  31538  cdlemg44  31544  cdlemg47  31547  ltrncom  31549  tendococl  31583  tendoplcl  31592  tendoplcom  31593  tendoplass  31594  tendodi1  31595  tendodi2  31596  tendo0pl  31602  tendoipl  31608  cdlemh1  31626  cdlemi2  31630  tendo0mul  31637  tendo0mulr  31638  cdlemk2  31643  cdlemk3  31644  cdlemk4  31645  cdlemk6  31648  cdlemk8  31649  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk5u  31672  cdlemk6u  31673  cdlemk12u  31683  cdlemkfid1N  31732  cdlemk19x  31754  cdlemk48  31761  cdlemk53a  31766  cdlemk56  31782  cdleml2N  31788  cdleml3N  31789  cdleml6  31792  cdleml7  31793  dva1dim  31796  dia2dimlem4  31879  dvhlveclem  31920  doca2N  31938  djajN  31949  cdlemn2a  32008  cdlemn3  32009  dihordlem6  32025  dihord5apre  32074  dihglbcpreN  32112  dihmeetcN  32114  dihmeetbN  32115  dihmeetlem10N  32128  dihmeetlem12N  32130  dihmeetlem15N  32133  dihmeetALTN  32139  dih1dimatlem0  32140  dihjatcclem3  32232  dihjatcclem4  32233  mapdpglem22  32505  hdmap14lem1a  32681
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator