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

Theorem syl121anc 1223
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 532 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1218 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 371  df-3an 967
This theorem is referenced by:  syl122anc  1227  disjxiun  4288  fsnunf2  5916  tfisi  6468  fnsuppeq0  6716  axdc4lem  8623  div32d  10129  div13d  10130  expdivd  12021  pcqmul  13919  pcid  13938  pcneg  13939  pc2dvds  13944  pcz  13946  pcaddlem  13949  pcadd  13950  pcmpt2  13954  pcbc  13961  qexpz  13962  expnprm  13963  sylow1lem1  16096  lspsneleq  17195  lspsneq  17202  lspfixed  17208  frlmsslss2  18198  ucncn  19859  ucnextcn  19878  ssblex  20002  prdsxmslem2  20103  voliunlem1  21030  deg1mul3le  21587  deg1pw  21591  fta1blem  21639  bcmono  22615  dchrisum0flblem1  22756  dchrisum0flblem2  22757  pntibndlem1  22837  pntlemr  22850  0wlkon  23445  0pthon  23477  nv1  24063  resf1o  26029  omndmul3  26175  measun  26624  measvuni  26627  measunl  26629  btwnconn1lem14  28130  segcon2  28135  seglelin  28146  neibastop3  28581  upixp  28621  fdc  28639  eldioph2b  29099  jm2.19lem4  29339  jm2.19  29340  jm2.26a  29347  jm2.26  29349  hbtlem2  29478  fnchoice  29749  stoweidlem42  29835  stoweidlem59  29852  clwlkfclwwlk  30515  pmatcollpw1dstlem1  30898  eqlkr3  32744  lkrshp  32748  lfl1dim  32764  lfl1dim2N  32765  eqlkr4  32808  2llnneN  33051  3dim2  33110  4atlem3  33238  4atlem11  33251  4atlem12  33254  pexmidlem4N  33615  lhp2at0nle  33677  lhple  33684  ltrnideq  33817  cdlemd9  33848  cdleme0ex2N  33866  cdleme0moN  33867  cdleme11a  33902  cdleme30a  34020  cdlemefs32sn1aw  34056  cdleme43fsv1snlem  34062  cdlemefs31fv1  34066  cdlemefs45eN  34073  cdleme41sn3a  34075  cdleme35h  34098  cdleme36a  34102  cdleme40m  34109  cdleme40n  34110  cdleme41sn3aw  34116  cdleme42h  34124  cdleme42k  34126  cdleme42mN  34129  cdleme43cN  34133  cdleme17d3  34138  cdleme48fvg  34142  cdlemeg47rv2  34152  cdlemeg46c  34155  cdlemeg46sfg  34162  cdlemeg46rjgN  34164  cdlemeg46rgv  34170  cdlemeg46req  34171  cdlemeg46gfv  34172  cdlemeg46gfre  34174  cdlemeg49lebilem  34181  cdleme50trn2  34193  cdlemg2kq  34244  cdlemb3  34248  cdlemg4f  34257  cdlemg9a  34274  cdlemg9b  34275  cdlemg9  34276  cdlemg11aq  34280  cdlemg12a  34285  cdlemg12b  34286  cdlemg12c  34287  cdlemg12d  34288  cdlemg12f  34290  cdlemg12g  34291  cdlemg12  34292  cdlemg13a  34293  cdlemg16  34299  cdlemg17e  34307  cdlemg17f  34308  cdlemg17g  34309  cdlemg17ir  34312  cdlemg17  34319  cdlemg18b  34321  cdlemg18c  34322  cdlemg33e  34352  trlcoabs2N  34364  trlcocnvat  34366  trlcolem  34368  trlco  34369  cdlemg44  34375  cdlemg47  34378  ltrncom  34380  tendococl  34414  tendoplcl  34423  tendoplcom  34424  tendoplass  34425  tendodi1  34426  tendodi2  34427  tendo0pl  34433  tendoipl  34439  cdlemh1  34457  cdlemi2  34461  tendo0mul  34468  tendo0mulr  34469  cdlemk2  34474  cdlemk3  34475  cdlemk4  34476  cdlemk6  34479  cdlemk8  34480  cdlemk12  34492  cdlemkole  34495  cdlemk14  34496  cdlemk15  34497  cdlemk5u  34503  cdlemk6u  34504  cdlemk12u  34514  cdlemkfid1N  34563  cdlemk19x  34585  cdlemk48  34592  cdlemk53a  34597  cdlemk56  34613  cdleml2N  34619  cdleml3N  34620  cdleml6  34623  cdleml7  34624  dva1dim  34627  dia2dimlem4  34710  dvhlveclem  34751  doca2N  34769  djajN  34780  cdlemn2a  34839  cdlemn3  34840  dihordlem6  34856  dihord5apre  34905  dihglbcpreN  34943  dihmeetcN  34945  dihmeetbN  34946  dihmeetlem10N  34959  dihmeetlem12N  34961  dihmeetlem15N  34964  dihmeetALTN  34970  dih1dimatlem0  34971  dihjatcclem3  35063  dihjatcclem4  35064  mapdpglem22  35336  hdmap14lem1a  35512
  Copyright terms: Public domain W3C validator