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

Theorem syl121anc 1231
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 530 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1226 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  syl122anc  1235  disjxiun  4436  fsnunf2  6086  tfisi  6666  fnsuppeq0  6920  axdc4lem  8826  div32d  10339  div13d  10340  expdivd  12306  swrdsbslen  12664  pcqmul  14461  pcid  14480  pcneg  14481  pc2dvds  14486  pcz  14488  pcaddlem  14491  pcadd  14492  pcmpt2  14496  pcbc  14503  qexpz  14504  expnprm  14505  sylow1lem1  16817  lspsneleq  17956  lspsneq  17963  lspfixed  17969  frlmsslss2  18976  chmatval  19497  chpmat1dlem  19503  chpdmatlem2  19507  ucncn  20954  ucnextcn  20973  ssblex  21097  prdsxmslem2  21198  voliunlem1  22126  deg1mul3le  22683  deg1pw  22687  fta1blem  22735  bcmono  23750  dchrisum0flblem1  23891  dchrisum0flblem2  23892  pntibndlem1  23972  pntlemr  23985  0wlkon  24751  0pthon  24783  clwlkfclwwlk  25046  nv1  25777  resf1o  27784  omndmul3  27937  rngurd  28013  measun  28419  measvuni  28422  measunl  28424  btwnconn1lem14  29978  segcon2  29983  seglelin  29994  neibastop3  30420  upixp  30460  fdc  30478  eldioph2b  30935  jm2.19lem4  31173  jm2.19  31174  jm2.26a  31181  jm2.26  31183  hbtlem2  31314  fnchoice  31644  stoweidlem42  32063  stoweidlem59  32080  fourierdlem42  32170  eqlkr3  35223  lkrshp  35227  lfl1dim  35243  lfl1dim2N  35244  eqlkr4  35287  2llnneN  35530  3dim2  35589  4atlem3  35717  4atlem11  35730  4atlem12  35733  pexmidlem4N  36094  lhp2at0nle  36156  lhple  36163  ltrnideq  36297  cdlemd9  36328  cdleme0ex2N  36346  cdleme0moN  36347  cdleme11a  36382  cdleme30a  36501  cdlemefs32sn1aw  36537  cdleme43fsv1snlem  36543  cdlemefs31fv1  36547  cdlemefs45eN  36554  cdleme41sn3a  36556  cdleme35h  36579  cdleme36a  36583  cdleme40m  36590  cdleme40n  36591  cdleme41sn3aw  36597  cdleme42h  36605  cdleme42k  36607  cdleme42mN  36610  cdleme43cN  36614  cdleme17d3  36619  cdleme48fvg  36623  cdlemeg47rv2  36633  cdlemeg46c  36636  cdlemeg46sfg  36643  cdlemeg46rjgN  36645  cdlemeg46rgv  36651  cdlemeg46req  36652  cdlemeg46gfv  36653  cdlemeg46gfre  36655  cdlemeg49lebilem  36662  cdleme50trn2  36674  cdlemg2kq  36725  cdlemb3  36729  cdlemg4f  36738  cdlemg9a  36755  cdlemg9b  36756  cdlemg9  36757  cdlemg11aq  36761  cdlemg12a  36766  cdlemg12b  36767  cdlemg12c  36768  cdlemg12d  36769  cdlemg12f  36771  cdlemg12g  36772  cdlemg12  36773  cdlemg13a  36774  cdlemg16  36780  cdlemg17e  36788  cdlemg17f  36789  cdlemg17g  36790  cdlemg17ir  36793  cdlemg17  36800  cdlemg18b  36802  cdlemg18c  36803  cdlemg33e  36833  trlcoabs2N  36845  trlcocnvat  36847  trlcolem  36849  trlco  36850  cdlemg44  36856  cdlemg47  36859  ltrncom  36861  tendococl  36895  tendoplcl  36904  tendoplcom  36905  tendoplass  36906  tendodi1  36907  tendodi2  36908  tendo0pl  36914  tendoipl  36920  cdlemh1  36938  cdlemi2  36942  tendo0mul  36949  tendo0mulr  36950  cdlemk2  36955  cdlemk3  36956  cdlemk4  36957  cdlemk6  36960  cdlemk8  36961  cdlemk12  36973  cdlemkole  36976  cdlemk14  36977  cdlemk15  36978  cdlemk5u  36984  cdlemk6u  36985  cdlemk12u  36995  cdlemkfid1N  37044  cdlemk19x  37066  cdlemk48  37073  cdlemk53a  37078  cdlemk56  37094  cdleml2N  37100  cdleml3N  37101  cdleml6  37104  cdleml7  37105  dva1dim  37108  dia2dimlem4  37191  dvhlveclem  37232  doca2N  37250  djajN  37261  cdlemn2a  37320  cdlemn3  37321  dihordlem6  37337  dihord5apre  37386  dihglbcpreN  37424  dihmeetcN  37426  dihmeetbN  37427  dihmeetlem10N  37440  dihmeetlem12N  37442  dihmeetlem15N  37445  dihmeetALTN  37451  dih1dimatlem0  37452  dihjatcclem3  37544  dihjatcclem4  37545  mapdpglem22  37817  hdmap14lem1a  37993
  Copyright terms: Public domain W3C validator