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  2095  equid1  2097  elex22  2799  elex2  2800  spcimdv  2865  spsbcd  3004  disjxiun  4020  opth  4245  euotd  4267  wereu  4389  wereu2  4390  tz7.7  4418  reusv2lem3  4537  ssorduni  4577  suceloni  4604  nlimsucg  4633  tfisi  4649  unielrel  5197  funmo  5271  iinpreima  5655  zfrep6  5748  fnfvima  5756  fliftfun  5811  fliftval  5815  weniso  5852  knatar  5857  ovmpt2dxf  5973  grprinvlem  6058  grprinvd  6059  caofref  6103  curry1  6210  curry2  6213  fnwelem  6230  riota5f  6329  riotass2  6332  smogt  6384  omeulem1  6580  oeworde  6591  oelimcl  6598  oeeulem  6599  oeeui  6600  nnawordex  6635  oaabs2  6643  ertr  6675  swoso  6691  qliftlem  6739  th3q  6767  resixp  6851  f1dom2g  6879  dom3d  6903  undom  6950  xpdom3  6960  domunsncan  6962  omxpenlem  6963  disjenex  7019  domssex2  7021  domssex  7022  xpf1o  7023  mapdom3  7033  findcard  7097  fiin  7175  marypha1lem  7186  marypha1  7187  fisupcl  7218  ordiso2  7230  ordtypelem2  7234  ordtypelem6  7238  ordtypelem7  7239  ordtypelem8  7240  wemapso2  7267  brwdom2  7287  unxpwdom2  7302  noinfepOLD  7361  cantnflt  7373  oemapvali  7386  cantnflem1d  7390  wemapwe  7400  cnfcom  7403  rankr1id  7534  tcrank  7554  cardmin2  7631  infxpenlem  7641  infxpenc2lem2  7647  fseqen  7654  dfac8clem  7659  ween  7662  ac5num  7663  indcardi  7668  acni  7672  acni2  7673  acnlem  7675  fodomfi2  7687  infpwfien  7689  inffien  7690  finnisoeu  7740  iunfictbso  7741  acacni  7766  dfac12lem2  7770  infpss  7843  infmap2  7844  ackbij1lem18  7863  ackbij1b  7865  fictb  7871  cfslb2n  7894  cofsmo  7895  cfsmolem  7896  coftr  7899  fin1ai  7919  fin2i  7921  infpssrlem4  7932  domfin4  7937  fin2i2  7944  isfin2-2  7945  fincssdom  7949  ssfin3ds  7956  fin23lem20  7963  fin23lem30  7968  isf32lem3  7981  fin1a2lem12  8037  fin1a2lem13  8038  hsmexlem2  8053  hsmexlem4  8055  axdc2lem  8074  axdc4lem  8081  ac6num  8106  ttukeylem6  8141  axdclem2  8147  imadomg  8159  iundom2g  8162  iundomg  8163  iundom  8164  unirnfdomd  8189  konigthlem  8190  iunctb  8196  fpwwe2  8265  canth4  8269  canthwelem  8272  pwfseqlem3  8282  pwfseqlem5  8285  winalim2  8318  wununi  8328  wunpw  8329  wunelss  8330  r1wunlim  8359  wunex2  8360  tsksdom  8378  tskinf  8391  inttsk  8396  inar1  8397  tskcard  8403  tskurn  8411  gruina  8440  grur1a  8441  grur1  8442  lemul12a  9614  lemulge11  9618  lediv12a  9649  nngt0  9775  peano5uzi  10100  nn0ind-raph  10112  zsupss  10307  suprzub  10309  uzsupss  10310  uzwo3  10311  rpge0  10366  fldiv  10964  uzrdgsuci  11023  fzennn  11030  uzindi  11043  seqcl2  11064  seqcl  11066  seqf  11067  seqfveq2  11068  seqfveq  11070  seqshft2  11072  monoord  11076  monoord2  11077  sermono  11078  seqsplit  11079  seqcaopr3  11081  seqid  11091  seqid2  11092  seqhomo  11093  seqz  11094  expcl2lem  11115  leexp1a  11160  modexp  11236  discr1  11237  discr  11238  faclbnd  11303  faclbnd6  11312  facavg  11314  hashginv  11341  hashbclem  11390  fz1isolem  11399  seqcoll  11401  resqrex  11736  cau3lem  11838  limsupgre  11955  climi  11984  rlimi  11987  rlimclim  12020  climrlim2  12021  rlimcld2  12052  rlimcn1  12062  climcn1  12065  climcn2  12066  isercoll  12141  isercoll2  12142  climsup  12143  caucvgrlem  12145  caurcvgr  12146  iseraltlem2  12155  iseraltlem3  12156  sumeq2ii  12166  summolem3  12187  fsum  12193  fsumadd  12211  fsumm1  12216  fsum1p  12218  fsum2dlem  12233  fsumcom2  12237  fsum0diag2  12245  fsummulc2  12246  fsumge1  12255  fsumabs  12259  fsumtscopo  12260  fsumtscopo2  12261  fsumparts  12264  fsumrelem  12265  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  qshash  12285  isum1p  12300  isumrpcl  12302  climcndslem1  12308  climcndslem2  12309  climcnds  12310  cvgrat  12339  mertenslem1  12340  mertens  12342  sin01gt0  12470  sin02gt0  12472  efieq1re  12479  divalglem9  12600  smupvallem  12674  rppwr  12736  algfx  12750  eucalgcvga  12756  prmind2  12769  qredeq  12785  pythagtriplem4  12872  pythagtriplem6  12874  pythagtriplem7  12875  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem14  12881  pythagtriplem16  12883  pcmpt  12940  pcmpt2  12941  prmpwdvds  12951  prmreclem2  12964  prmreclem4  12966  prmreclem5  12967  4sqlem11  13002  vdwlem1  13028  vdwlem2  13029  vdwlem9  13036  vdwlem10  13037  vdwlem11  13038  vdwlem12  13039  rami  13062  0ram  13067  0ram2  13068  0ramcl  13070  ramcl  13076  prmlem1  13109  prmlem2  13121  strfvd  13177  strfv2d  13178  strssd  13182  firest  13337  prdsdsval3  13384  imasbas  13415  imasds  13416  imasaddfnlem  13430  imasaddvallem  13431  imasvscafn  13439  divsaddvallem  13453  divsaddflem  13454  divsaddval  13455  divsaddf  13456  divsmulval  13457  divsmulf  13458  isacs1i  13559  mreacs  13560  catidex  13576  catideu  13577  iscatd2  13583  catlid  13585  catrid  13586  subcidcl  13718  funcid  13744  invfuc  13848  yonedalem4c  14051  yonffthlem  14056  mod2ile  14212  lubss  14225  acsmapd  14281  gsumval2a  14459  grpidd2  14519  mulgnegnn  14577  mulgsubcl  14581  divsgrp2  14613  issubg4  14638  ghmf1  14711  pgpssslw  14925  sylow2alem2  14929  fislw  14936  efgsdmi  15041  efgsrel  15043  efgsres  15047  gexexlem  15144  gsumval3  15191  gsumzaddlem  15203  gsummhm2  15212  gsum2d  15223  dprdcntz  15243  dprddisj  15244  dprdss  15264  dprd2dlem2  15275  dprd2da  15277  dpjrid  15297  ablfac1eu  15308  pgpfac1lem1  15309  ablfac2  15324  rngi  15353  divsrng2  15403  issrngd  15626  lssintcl  15721  islbs2  15907  lbsextlem3  15913  lbsextlem4  15914  mplsubglem  16179  mpllsslem  16180  subrgasclcl  16240  zlpirlem3  16443  eltg3  16700  cctop  16743  subbascn  16984  iscncl  16998  cnss2  17006  cnrmi  17088  cmpcov  17116  cmpcovf  17118  fiuncmp  17131  2ndcctbss  17181  2ndcomap  17184  2ndcsep  17185  1stcelcls  17187  islly2  17210  ptpjpre1  17266  elptr  17268  ptbasfi  17276  ptpjopn  17306  ptclsg  17309  dfac14  17312  txcnp  17314  ptcnplem  17315  uptx  17319  txtube  17334  tx2ndc  17345  xkococnlem  17353  cnmpt11  17357  cnmpt21  17365  cnmptkp  17374  cnmptk1p  17379  elqtop  17388  qtoprest  17408  qtopomap  17409  qtopcmap  17410  indishmph  17489  ptcmpfi  17504  kqhmph  17510  csdfil  17589  filssufilg  17606  ufilen  17625  rnelfm  17648  fmfnfmlem4  17652  flimcf  17677  fclscf  17720  alexsubALTlem4  17744  ptcmplem3  17748  ptcmplem4  17749  tmdgsum2  17779  tsmsxplem2  17836  imasdsf1olem  17937  imasf1oxmet  17939  metss  18054  comet  18059  met2ndci  18068  prdsxmslem2  18075  opnreen  18336  rectbntr0  18337  fsumcn  18374  rescncf  18401  xrhmeo  18444  cnheiborlem  18452  cnheibor  18453  cnllycmp  18454  lebnumlem1  18459  lebnumlem3  18461  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  lmmcvg  18687  cfilss  18696  iscmet3lem1  18717  iscmet3lem2  18718  pjthlem1  18801  pjthlem2  18802  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  ivth2  18815  ivthle  18816  ivthle2  18817  ivthicc  18818  ovolsslem  18843  ovoliunlem1  18861  ovoliunlem2  18862  ovoliunnul  18866  ovolshftlem1  18868  ovolscalem1  18872  ovolicc2lem3  18878  ovolicc2lem4  18879  voliunlem3  18909  volsup  18913  uniiccdif  18933  uniioombllem2  18938  dyadmbl  18955  volivth  18962  vitalilem3  18965  ismbf3d  19009  mbfimaopnlem  19010  cncombf  19013  mbflimsup  19021  i1fd  19036  itg1addlem4  19054  itg2addlem  19113  itg2gt0  19115  iblitg  19123  itgconst  19173  itgfsum  19181  limcvallem  19221  cnlimci  19239  cnmptlimc  19240  limciun  19244  dvadd  19289  dvmul  19290  dvco  19296  dvrec  19304  dvcnv  19324  dvferm1lem  19331  dvferm1  19332  dvferm2lem  19333  dvferm2  19334  dvferm  19335  rollelem  19336  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  c1lip2  19345  dvgt0lem1  19349  dvle  19354  dvivthlem1  19355  lhop1lem  19360  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcvx  19367  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlim2  19379  dvfsum2  19381  ftc1cn  19390  ftc2ditglem  19392  itgsubstlem  19395  evlslem3  19398  evlseu  19400  mpfpf1  19434  pf1mpf  19435  tdeglem4  19446  mdegaddle  19460  mdegmullem  19464  deg1sublt  19496  ply1divmo  19521  fta1g  19553  dgrub  19616  dgradd2  19649  dvply1  19664  plydivex  19677  plyrem  19685  vieta1lem2  19691  aalioulem4  19715  aalioulem5  19716  aalioulem6  19717  aaliou2  19720  taylf  19740  tayl0  19741  ulmi  19765  ulmdvlem1  19777  ulmdvlem3  19779  ulmdv  19780  mtest  19781  pserulm  19798  psercn2  19799  abelth  19817  abelth2  19818  reeff1olem  19822  efif1olem4  19907  efopn  20005  logreclem  20116  isosctrlem2  20119  rlimcnp  20260  rlimcnp2  20261  xrlimcnp  20263  scvxcvx  20280  wilthlem2  20307  basellem4  20321  ppiwordi  20400  fsumdvdscom  20425  musum  20431  musumsum  20432  chtub  20451  fsumvma  20452  chpub  20459  dchrelbas3  20477  dchrelbasd  20478  dchrn0  20489  dchrptlem2  20504  lgsval2lem  20545  lgsdirnn0  20578  lgsdinn0  20579  2sqlem6  20608  2sqlem10  20613  dchrisumlema  20637  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  dchrisum0flb  20659  dchrisum0re  20662  dchrisum0lem1b  20664  dchrisum0lem2  20667  2vmadivsumlem  20689  chpdifbndlem1  20702  selberg3lem1  20706  selberg4lem1  20709  pntrsumbnd2  20716  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntibndlem2  20740  pntibndlem3  20741  pntlemn  20749  pntlemj  20752  pntlemi  20753  pntlemo  20756  pntlem3  20758  pntlemp  20759  pntleml  20760  ostth2lem1  20767  ostth2lem2  20783  ostth3  20787  isgrp2d  20902  opidon  20989  ghgrp  21035  rngodm1dm2  21085  ubthlem1  21449  ubthlem2  21450  minvecolem3  21455  minvecolem4b  21457  minvecolem4  21459  bcsiALT  21758  occllem  21882  pjhthlem1  21970  ococin  21987  spanpr  22159  pjorthi  22248  nmbdoplbi  22604  nmcoplbi  22608  nmbdfnlbi  22629  nmcfnlbi  22632  nmopcoi  22675  branmfn  22685  hstnmoc  22803  mdsl0  22890  atomli  22962  atcvat4i  22977  atabsi  22981  ifeqeqx  23034  ballotlemfp1  23050  ballotlemfrcn0  23088  abrexdomjm  23165  fovcld  23203  xlt2addrd  23253  supxrnemnf  23256  ssnnssfz  23277  fnct  23341  esumcst  23436  esumpinfval  23441  esumpinfsum  23445  sigaclci  23493  insiga  23498  measres  23549  measdivcstOLD  23551  measdivcst  23552  mbfmcnvima  23562  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  rescon  23777  cvmliftlem3  23818  cvmlift2lem10  23843  relexpadd  24035  relexpindlem  24036  rtrclreclem.trans  24043  dedekind  24082  wfrlem4  24259  wfrlem15  24270  frrlem4  24284  sltres  24318  nobndlem2  24347  nobndup  24354  nobnddown  24355  nofulllem3  24358  nofulllem5  24360  axlowdimlem16  24585  axlowdimlem17  24586  axcontlem3  24594  axcontlem10  24601  cgrextend  24631  segconeq  24633  trisegint  24651  ontgval  24870  wl-bitrd  24912  sndw  25100  ordsuccl3  25104  injrec2  25119  surjsec2  25120  cbicp  25166  prl  25167  jidd  25192  midd  25193  preoref22  25229  ubos  25256  supdefa  25263  geme2  25275  dfps2  25289  dffprod  25319  trinv  25395  ltrinvlem  25406  rngodmeqrn  25419  zerdivemp1  25436  intopcoaconlem3  25539  exopcopn  25572  islimrs3  25581  lvsovso  25626  lvsovso3  25628  supnuf  25629  intvconlem1  25703  rdmob  25748  cmpassoh  25801  homgrf  25802  cmpmon  25815  idmon  25817  immon  25818  idsubfun  25858  inttaror  25900  cmpmor  25975  elhaltdp2  26068  sgplpte21b  26134  sgplpte21d1  26139  sgplpte21d2  26140  ivthALT  26258  fnessref  26293  refssfne  26294  comppfsc  26307  neibastop1  26308  filnetlem4  26330  abrexdom  26405  indexdom  26413  mettrifi  26473  equivtotbnd  26502  totbndbnd  26513  prdstotbnd  26518  heibor1lem  26533  bfplem1  26546  bfplem2  26547  zerdivemp1x  26586  ofmpteq  26797  mzpsubmpt  26821  mzpsubst  26826  eqrabdioph  26857  rabdiophlem2  26883  elpell14qr2  26947  elpell1qr2  26957  pellfundre  26966  pellfundge  26967  pellfundglb  26970  pellfundex  26971  pellfund14gap  26972  monotoddzzfi  27027  congabseq  27061  dvdsleabs2  27077  jm2.22  27088  jm2.23  27089  jm2.26lem3  27094  wepwsolem  27138  dnwech  27145  aomclem2  27152  aomclem4  27154  frlmup4  27253  lindff1  27290  lindfrn  27291  lmisfree  27312  dgrnznn  27340  symggen  27411  psgnunilem4  27420  sbiota1  27634  refsumcn  27701  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  cncfmptss  27717  climmulf  27730  climinf  27732  climsuselem1  27733  climsuse  27734  stoweidlem1  27750  stoweidlem3  27752  stoweidlem16  27765  stoweidlem18  27767  stoweidlem19  27768  stoweidlem22  27771  stoweidlem24  27773  stoweidlem25  27774  stoweidlem31  27780  stoweidlem34  27783  stoweidlem42  27791  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  stoweid  27812  wallispilem1  27814  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2  27822  f1oun2prg  28076  s2f1o  28091  nbgrassovt  28150  ordelordALT  28301  2pm13.193  28318  ee11an  28462  bnj1379  28863  bnj580  28945  bnj944  28970  bnj999  28989  bnj1204  29042  bnj1398  29064  bnj1491  29087  ax12-4  29106  a12study4  29117  omllaw5N  29437  cmtcomlemN  29438  cmtbr3N  29444  omlfh3N  29449  atlen0  29500  exatleN  29593  hlrelat3  29601  cvrexchlem  29608  atlelt  29627  cvrat4  29632  4atlem11b  29797  4atlem12b  29800  lneq2at  29967  cdlema1N  29980  cdlemblem  29982  paddss12  30008  paddasslem2  30010  paddasslem4  30012  paddasslem6  30014  paddasslem12  30020  paddunN  30116  poml4N  30142  poml5N  30143  osumcllem6N  30150  pexmidlem6N  30164  pl42lem2N  30169  ltrnu  30310  ltrneq2  30337  trlval2  30352  cdlemd6  30392  cdleme25b  30543  cdleme29b  30564  cdlemefr29exN  30591  ltrniotacnvval  30771  cdlemk28-3  31097  dochexmidlem7  31656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator