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

Theorem sylc 56
Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)
Hypotheses
Ref Expression
sylc.1  |-  ( ph  ->  ps )
sylc.2  |-  ( ph  ->  ch )
sylc.3  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
sylc  |-  ( ph  ->  th )

Proof of Theorem sylc
StepHypRef Expression
1 sylc.1 . . 3  |-  ( ph  ->  ps )
2 sylc.2 . . 3  |-  ( ph  ->  ch )
3 sylc.3 . . 3  |-  ( ps 
->  ( ch  ->  th )
)
41, 2, 3syl2im 34 . 2  |-  ( ph  ->  ( ph  ->  th )
)
54pm2.43i 43 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl3c  57  mpsyl  59  jc  139  2thd  231  jca  518  syl2anc  642  ax12  1888  ax12from12o  2108  equid1  2110  elex22  2812  elex2  2813  spcimdv  2878  spsbcd  3017  disjxiun  4036  opth  4261  euotd  4283  wereu  4405  wereu2  4406  tz7.7  4434  reusv2lem3  4553  ssorduni  4593  suceloni  4620  nlimsucg  4649  tfisi  4665  unielrel  5213  funmo  5287  iinpreima  5671  zfrep6  5764  fnfvima  5772  fliftfun  5827  fliftval  5831  weniso  5868  knatar  5873  ovmpt2dxf  5989  grprinvlem  6074  grprinvd  6075  caofref  6119  curry1  6226  curry2  6229  fnwelem  6246  riota5f  6345  riotass2  6348  smogt  6400  omeulem1  6596  oeworde  6607  oelimcl  6614  oeeulem  6615  oeeui  6616  nnawordex  6651  oaabs2  6659  ertr  6691  swoso  6707  qliftlem  6755  th3q  6783  resixp  6867  f1dom2g  6895  dom3d  6919  undom  6966  xpdom3  6976  domunsncan  6978  omxpenlem  6979  disjenex  7035  domssex2  7037  domssex  7038  xpf1o  7039  mapdom3  7049  findcard  7113  fiin  7191  marypha1lem  7202  marypha1  7203  fisupcl  7234  ordiso2  7246  ordtypelem2  7250  ordtypelem6  7254  ordtypelem7  7255  ordtypelem8  7256  wemapso2  7283  brwdom2  7303  unxpwdom2  7318  noinfepOLD  7377  cantnflt  7389  oemapvali  7402  cantnflem1d  7406  wemapwe  7416  cnfcom  7419  rankr1id  7550  tcrank  7570  cardmin2  7647  infxpenlem  7657  infxpenc2lem2  7663  fseqen  7670  dfac8clem  7675  ween  7678  ac5num  7679  indcardi  7684  acni  7688  acni2  7689  acnlem  7691  fodomfi2  7703  infpwfien  7705  inffien  7706  finnisoeu  7756  iunfictbso  7757  acacni  7782  dfac12lem2  7786  infpss  7859  infmap2  7860  ackbij1lem18  7879  ackbij1b  7881  fictb  7887  cfslb2n  7910  cofsmo  7911  cfsmolem  7912  coftr  7915  fin1ai  7935  fin2i  7937  infpssrlem4  7948  domfin4  7953  fin2i2  7960  isfin2-2  7961  fincssdom  7965  ssfin3ds  7972  fin23lem20  7979  fin23lem30  7984  isf32lem3  7997  fin1a2lem12  8053  fin1a2lem13  8054  hsmexlem2  8069  hsmexlem4  8071  axdc2lem  8090  axdc4lem  8097  ac6num  8122  ttukeylem6  8157  axdclem2  8163  imadomg  8175  iundom2g  8178  iundomg  8179  iundom  8180  unirnfdomd  8205  konigthlem  8206  iunctb  8212  fpwwe2  8281  canth4  8285  canthwelem  8288  pwfseqlem3  8298  pwfseqlem5  8301  winalim2  8334  wununi  8344  wunpw  8345  wunelss  8346  r1wunlim  8375  wunex2  8376  tsksdom  8394  tskinf  8407  inttsk  8412  inar1  8413  tskcard  8419  tskurn  8427  gruina  8456  grur1a  8457  grur1  8458  lemul12a  9630  lemulge11  9634  lediv12a  9665  nngt0  9791  peano5uzi  10116  nn0ind-raph  10128  zsupss  10323  suprzub  10325  uzsupss  10326  uzwo3  10327  rpge0  10382  fldiv  10980  uzrdgsuci  11039  fzennn  11046  uzindi  11059  seqcl2  11080  seqcl  11082  seqf  11083  seqfveq2  11084  seqfveq  11086  seqshft2  11088  monoord  11092  monoord2  11093  sermono  11094  seqsplit  11095  seqcaopr3  11097  seqid  11107  seqid2  11108  seqhomo  11109  seqz  11110  expcl2lem  11131  leexp1a  11176  modexp  11252  discr1  11253  discr  11254  faclbnd  11319  faclbnd6  11328  facavg  11330  hashginv  11357  hashbclem  11406  fz1isolem  11415  seqcoll  11417  resqrex  11752  cau3lem  11854  limsupgre  11971  climi  12000  rlimi  12003  rlimclim  12036  climrlim2  12037  rlimcld2  12068  rlimcn1  12078  climcn1  12081  climcn2  12082  isercoll  12157  isercoll2  12158  climsup  12159  caucvgrlem  12161  caurcvgr  12162  iseraltlem2  12171  iseraltlem3  12172  sumeq2ii  12182  summolem3  12203  fsum  12209  fsumadd  12227  fsumm1  12232  fsum1p  12234  fsum2dlem  12249  fsumcom2  12253  fsum0diag2  12261  fsummulc2  12262  fsumge1  12271  fsumabs  12275  fsumtscopo  12276  fsumtscopo2  12277  fsumparts  12280  fsumrelem  12281  fsumrlim  12285  fsumo1  12286  o1fsum  12287  fsumiun  12295  qshash  12301  isum1p  12316  isumrpcl  12318  climcndslem1  12324  climcndslem2  12325  climcnds  12326  cvgrat  12355  mertenslem1  12356  mertens  12358  sin01gt0  12486  sin02gt0  12488  efieq1re  12495  divalglem9  12616  smupvallem  12690  rppwr  12752  algfx  12766  eucalgcvga  12772  prmind2  12785  qredeq  12801  pythagtriplem4  12888  pythagtriplem6  12890  pythagtriplem7  12891  pythagtriplem12  12895  pythagtriplem13  12896  pythagtriplem14  12897  pythagtriplem16  12899  pcmpt  12956  pcmpt2  12957  prmpwdvds  12967  prmreclem2  12980  prmreclem4  12982  prmreclem5  12983  4sqlem11  13018  vdwlem1  13044  vdwlem2  13045  vdwlem9  13052  vdwlem10  13053  vdwlem11  13054  vdwlem12  13055  rami  13078  0ram  13083  0ram2  13084  0ramcl  13086  ramcl  13092  prmlem1  13125  prmlem2  13137  strfvd  13193  strfv2d  13194  strssd  13198  firest  13353  prdsdsval3  13400  imasbas  13431  imasds  13432  imasaddfnlem  13446  imasaddvallem  13447  imasvscafn  13455  divsaddvallem  13469  divsaddflem  13470  divsaddval  13471  divsaddf  13472  divsmulval  13473  divsmulf  13474  isacs1i  13575  mreacs  13576  catidex  13592  catideu  13593  iscatd2  13599  catlid  13601  catrid  13602  subcidcl  13734  funcid  13760  invfuc  13864  yonedalem4c  14067  yonffthlem  14072  mod2ile  14228  lubss  14241  acsmapd  14297  gsumval2a  14475  grpidd2  14535  mulgnegnn  14593  mulgsubcl  14597  divsgrp2  14629  issubg4  14654  ghmf1  14727  pgpssslw  14941  sylow2alem2  14945  fislw  14952  efgsdmi  15057  efgsrel  15059  efgsres  15063  gexexlem  15160  gsumval3  15207  gsumzaddlem  15219  gsummhm2  15228  gsum2d  15239  dprdcntz  15259  dprddisj  15260  dprdss  15280  dprd2dlem2  15291  dprd2da  15293  dpjrid  15313  ablfac1eu  15324  pgpfac1lem1  15325  ablfac2  15340  rngi  15369  divsrng2  15419  issrngd  15642  lssintcl  15737  islbs2  15923  lbsextlem3  15929  lbsextlem4  15930  mplsubglem  16195  mpllsslem  16196  subrgasclcl  16256  zlpirlem3  16459  eltg3  16716  cctop  16759  subbascn  17000  iscncl  17014  cnss2  17022  cnrmi  17104  cmpcov  17132  cmpcovf  17134  fiuncmp  17147  2ndcctbss  17197  2ndcomap  17200  2ndcsep  17201  1stcelcls  17203  islly2  17226  ptpjpre1  17282  elptr  17284  ptbasfi  17292  ptpjopn  17322  ptclsg  17325  dfac14  17328  txcnp  17330  ptcnplem  17331  uptx  17335  txtube  17350  tx2ndc  17361  xkococnlem  17369  cnmpt11  17373  cnmpt21  17381  cnmptkp  17390  cnmptk1p  17395  elqtop  17404  qtoprest  17424  qtopomap  17425  qtopcmap  17426  indishmph  17505  ptcmpfi  17520  kqhmph  17526  csdfil  17605  filssufilg  17622  ufilen  17641  rnelfm  17664  fmfnfmlem4  17668  flimcf  17693  fclscf  17736  alexsubALTlem4  17760  ptcmplem3  17764  ptcmplem4  17765  tmdgsum2  17795  tsmsxplem2  17852  imasdsf1olem  17953  imasf1oxmet  17955  metss  18070  comet  18075  met2ndci  18084  prdsxmslem2  18091  opnreen  18352  rectbntr0  18353  fsumcn  18390  rescncf  18417  xrhmeo  18460  cnheiborlem  18468  cnheibor  18469  cnllycmp  18470  lebnumlem1  18475  lebnumlem3  18477  ipcau2  18680  tchcphlem1  18681  tchcphlem2  18682  lmmcvg  18703  cfilss  18712  iscmet3lem1  18733  iscmet3lem2  18734  pjthlem1  18817  pjthlem2  18818  ivthlem1  18827  ivthlem2  18828  ivthlem3  18829  ivth2  18831  ivthle  18832  ivthle2  18833  ivthicc  18834  ovolsslem  18859  ovoliunlem1  18877  ovoliunlem2  18878  ovoliunnul  18882  ovolshftlem1  18884  ovolscalem1  18888  ovolicc2lem3  18894  ovolicc2lem4  18895  voliunlem3  18925  volsup  18929  uniiccdif  18949  uniioombllem2  18954  dyadmbl  18971  volivth  18978  vitalilem3  18981  ismbf3d  19025  mbfimaopnlem  19026  cncombf  19029  mbflimsup  19037  i1fd  19052  itg1addlem4  19070  itg2addlem  19129  itg2gt0  19131  iblitg  19139  itgconst  19189  itgfsum  19197  limcvallem  19237  cnlimci  19255  cnmptlimc  19256  limciun  19260  dvadd  19305  dvmul  19306  dvco  19312  dvrec  19320  dvcnv  19340  dvferm1lem  19347  dvferm1  19348  dvferm2lem  19349  dvferm2  19350  dvferm  19351  rollelem  19352  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  c1lip2  19361  dvgt0lem1  19365  dvle  19370  dvivthlem1  19371  lhop1lem  19376  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcvx  19383  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvfsumlem1  19389  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlim2  19395  dvfsum2  19397  ftc1cn  19406  ftc2ditglem  19408  itgsubstlem  19411  evlslem3  19414  evlseu  19416  mpfpf1  19450  pf1mpf  19451  tdeglem4  19462  mdegaddle  19476  mdegmullem  19480  deg1sublt  19512  ply1divmo  19537  fta1g  19569  dgrub  19632  dgradd2  19665  dvply1  19680  plydivex  19693  plyrem  19701  vieta1lem2  19707  aalioulem4  19731  aalioulem5  19732  aalioulem6  19733  aaliou2  19736  taylf  19756  tayl0  19757  ulmi  19781  ulmdvlem1  19793  ulmdvlem3  19795  ulmdv  19796  mtest  19797  pserulm  19814  psercn2  19815  abelth  19833  abelth2  19834  reeff1olem  19838  efif1olem4  19923  efopn  20021  logreclem  20132  isosctrlem2  20135  rlimcnp  20276  rlimcnp2  20277  xrlimcnp  20279  scvxcvx  20296  wilthlem2  20323  basellem4  20337  ppiwordi  20416  fsumdvdscom  20441  musum  20447  musumsum  20448  chtub  20467  fsumvma  20468  chpub  20475  dchrelbas3  20493  dchrelbasd  20494  dchrn0  20505  dchrptlem2  20520  lgsval2lem  20561  lgsdirnn0  20594  lgsdinn0  20595  2sqlem6  20624  2sqlem10  20629  dchrisumlema  20653  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  dchrmusum2  20659  dchrvmasumlem2  20663  dchrvmasumlem3  20664  dchrvmasumiflem1  20666  dchrisum0flblem2  20674  dchrisum0flb  20675  dchrisum0re  20678  dchrisum0lem1b  20680  dchrisum0lem2  20683  2vmadivsumlem  20705  chpdifbndlem1  20718  selberg3lem1  20722  selberg4lem1  20725  pntrsumbnd2  20732  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntibndlem2  20756  pntibndlem3  20757  pntlemn  20765  pntlemj  20768  pntlemi  20769  pntlemo  20772  pntlem3  20774  pntlemp  20775  pntleml  20776  ostth2lem1  20783  ostth2lem2  20799  ostth3  20803  isgrp2d  20918  opidon  21005  ghgrp  21051  rngodm1dm2  21101  ubthlem1  21465  ubthlem2  21466  minvecolem3  21471  minvecolem4b  21473  minvecolem4  21475  bcsiALT  21774  occllem  21898  pjhthlem1  21986  ococin  22003  spanpr  22175  pjorthi  22264  nmbdoplbi  22620  nmcoplbi  22624  nmbdfnlbi  22645  nmcfnlbi  22648  nmopcoi  22691  branmfn  22701  hstnmoc  22819  mdsl0  22906  atomli  22978  atcvat4i  22993  atabsi  22997  ifeqeqx  23050  ballotlemfp1  23066  ballotlemfrcn0  23104  abrexdomjm  23181  fovcld  23218  xlt2addrd  23268  supxrnemnf  23271  ssnnssfz  23292  fnct  23356  esumcst  23451  esumpinfval  23456  esumpinfsum  23460  sigaclci  23508  insiga  23513  measres  23564  measdivcstOLD  23566  measdivcst  23567  mbfmcnvima  23577  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  rescon  23792  cvmliftlem3  23833  cvmlift2lem10  23858  relexpadd  24050  relexpindlem  24051  rtrclreclem.trans  24058  dedekind  24097  cprodeq2ii  24135  prodmolem3  24156  fprod  24164  wfrlem4  24330  wfrlem15  24341  frrlem4  24355  sltres  24389  nobndlem2  24418  nobndup  24425  nobnddown  24426  nofulllem3  24429  nofulllem5  24431  axlowdimlem16  24657  axlowdimlem17  24658  axcontlem3  24666  axcontlem10  24673  cgrextend  24703  segconeq  24705  trisegint  24723  ontgval  24942  wl-bitrd  24984  ftc1cnnclem  25024  ftc1cnnc  25025  sndw  25203  ordsuccl3  25207  injrec2  25222  surjsec2  25223  cbicp  25269  prl  25270  jidd  25295  midd  25296  preoref22  25332  ubos  25359  supdefa  25366  geme2  25378  dfps2  25392  dffprod  25422  trinv  25498  ltrinvlem  25509  rngodmeqrn  25522  zerdivemp1  25539  intopcoaconlem3  25642  exopcopn  25675  islimrs3  25684  lvsovso  25729  lvsovso3  25731  supnuf  25732  intvconlem1  25806  rdmob  25851  cmpassoh  25904  homgrf  25905  cmpmon  25918  idmon  25920  immon  25921  idsubfun  25961  inttaror  26003  cmpmor  26078  elhaltdp2  26171  sgplpte21b  26237  sgplpte21d1  26242  sgplpte21d2  26243  ivthALT  26361  fnessref  26396  refssfne  26397  comppfsc  26410  neibastop1  26411  filnetlem4  26433  abrexdom  26508  indexdom  26516  mettrifi  26576  equivtotbnd  26605  totbndbnd  26616  prdstotbnd  26621  heibor1lem  26636  bfplem1  26649  bfplem2  26650  zerdivemp1x  26689  ofmpteq  26900  mzpsubmpt  26924  mzpsubst  26929  eqrabdioph  26960  rabdiophlem2  26986  elpell14qr2  27050  elpell1qr2  27060  pellfundre  27069  pellfundge  27070  pellfundglb  27073  pellfundex  27074  pellfund14gap  27075  monotoddzzfi  27130  congabseq  27164  dvdsleabs2  27180  jm2.22  27191  jm2.23  27192  jm2.26lem3  27197  wepwsolem  27241  dnwech  27248  aomclem2  27255  aomclem4  27257  frlmup4  27356  lindff1  27393  lindfrn  27394  lmisfree  27415  dgrnznn  27443  symggen  27514  psgnunilem4  27523  sbiota1  27737  refsumcn  27804  fmul01  27813  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  cncfmptss  27820  climmulf  27833  climinf  27835  climsuselem1  27836  climsuse  27837  stoweidlem1  27853  stoweidlem3  27855  stoweidlem16  27868  stoweidlem18  27870  stoweidlem19  27871  stoweidlem22  27874  stoweidlem24  27876  stoweidlem25  27877  stoweidlem31  27883  stoweidlem34  27886  stoweidlem42  27894  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem57  27909  stoweidlem59  27911  stoweidlem60  27912  stoweidlem62  27914  stoweid  27915  wallispilem1  27917  wallispilem3  27919  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2  27925  f1oun2prg  28187  s2f1o  28223  nbgrassovt  28284  ordelordALT  28600  2pm13.193  28617  ee11an  28767  bnj1379  29179  bnj580  29261  bnj944  29286  bnj999  29305  bnj1204  29358  bnj1398  29380  bnj1491  29403  ax12-4  29728  a12study4  29739  omllaw5N  30059  cmtcomlemN  30060  cmtbr3N  30066  omlfh3N  30071  atlen0  30122  exatleN  30215  hlrelat3  30223  cvrexchlem  30230  atlelt  30249  cvrat4  30254  4atlem11b  30419  4atlem12b  30422  lneq2at  30589  cdlema1N  30602  cdlemblem  30604  paddss12  30630  paddasslem2  30632  paddasslem4  30634  paddasslem6  30636  paddasslem12  30642  paddunN  30738  poml4N  30764  poml5N  30765  osumcllem6N  30772  pexmidlem6N  30786  pl42lem2N  30791  ltrnu  30932  ltrneq2  30959  trlval2  30974  cdlemd6  31014  cdleme25b  31165  cdleme29b  31186  cdlemefr29exN  31213  ltrniotacnvval  31393  cdlemk28-3  31719  dochexmidlem7  32278
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator