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

Theorem sylc 65
Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)
Hypotheses
Ref Expression
sylc.1 (𝜑𝜓)
sylc.2 (𝜑𝜒)
sylc.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
sylc (𝜑𝜃)

Proof of Theorem sylc
StepHypRef Expression
1 sylc.1 . . 3 (𝜑𝜓)
2 sylc.2 . . 3 (𝜑𝜒)
3 sylc.3 . . 3 (𝜓 → (𝜒𝜃))
41, 2, 3syl2im 40 . 2 (𝜑 → (𝜑𝜃))
54pm2.43i 52 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl3c  66  mpsyl  68  jc  164  jcnd  166  2thd  268  jca  515  syl2anc  587  unitreslOLD  875  aevlem0  2059  equvel  2471  elex2  3466  elex22  3467  spcedv  3550  rspcdf  3561  rspcdva  3576  spsbcd  3737  opth  5336  euotd  5371  wereu2  5520  unielrel  6097  tz7.7  6189  funmo  6344  fvelimad  6711  iinpreima  6818  fnfvima  6977  resfvresima  6979  fliftfun  7048  fliftval  7052  weniso  7090  riota5f  7125  riotass2  7127  ofmpteq  7412  ssorduni  7484  suceloni  7512  nlimsucg  7541  tfisi  7557  zfrep6  7642  curry1  7786  curry2  7789  fnwelem  7812  funsssuppss  7843  wfrlem4  7945  smogt  7991  tfrlem5  8003  omeulem1  8195  oeworde  8206  oelimcl  8213  oeeulem  8214  oeeui  8215  nnawordex  8250  oaabs2  8259  swoso  8309  qliftlem  8365  resixp  8484  undom  8592  xpdom3  8602  domunsncan  8604  omxpenlem  8605  domssex  8666  xpf1o  8667  mapdom3  8677  findcard  8745  f1dmvrnfibi  8796  fiin  8874  marypha1lem  8885  marypha1  8886  fisupcl  8921  supgtoreq  8922  ordiso2  8967  ordtypelem2  8971  ordtypelem8  8977  wemapso2lem  9004  unxpwdom2  9040  cantnflt  9123  cantnfrescl  9127  oemapvali  9135  cantnflem1d  9139  wemapwe  9148  cnfcom  9151  rankr1id  9279  tcrank  9301  cardmin2  9416  infxpenlem  9428  fseqen  9442  ween  9450  ac5num  9451  indcardi  9456  acni2  9461  fodomfi2  9475  infpwfien  9477  inffien  9478  iunfictbso  9529  acacni  9555  dfac12lem2  9559  djuinf  9603  infmap2  9633  ackbij1lem18  9652  ackbij1b  9654  fictb  9660  cfslb2n  9683  cofsmo  9684  cfsmolem  9685  coftr  9688  infpssrlem4  9721  domfin4  9726  fin2i2  9733  isfin2-2  9734  fincssdom  9738  ssfin3ds  9745  fin23lem20  9752  fin23lem30  9757  isf32lem3  9770  fin1a2lem12  9826  fin1a2lem13  9827  hsmexlem2  9842  axdc2lem  9863  imadomg  9949  fnct  9952  iundom2g  9955  iundomg  9956  iundom  9957  unirnfdomd  9982  konigthlem  9983  iunctb  9989  fpwwe2  10058  canthwelem  10065  pwfseqlem3  10075  pwfseqlem5  10078  winalim2  10111  wunelss  10123  r1wunlim  10152  wunex2  10153  tsksdom  10171  tskinf  10184  inttsk  10189  inar1  10190  tskcard  10196  tskurn  10204  gruina  10233  grur1a  10234  grur1  10235  addsrpr  10490  mulsrpr  10491  lemul12a  11491  lemulge11  11495  lediv12a  11526  nngt0  11660  nn0ge2m1nn  11956  peano5uzi  12063  nn0ind-raph  12074  znnn0nn  12086  suprzub  12331  uzsupss  12332  rpge0  12394  fz0fzelfz0  13012  fz0fzdiffz0  13015  ige2m2fzo  13099  elfzodifsumelfzo  13102  elfzom1elp1fzo  13103  fzonfzoufzol  13139  flltdivnn0lt  13202  fldiv  13227  modaddmodup  13301  uzrdgsuci  13327  fzennn  13335  uzindi  13349  fsuppmapnn0fiubex  13359  expcl2lem  13441  leexp1a  13539  modexp  13599  faclbnd  13650  faclbnd6  13659  facavg  13661  hashginv  13694  hashf1rn  13713  hasheqf1od  13714  seqcoll  13822  hashge2el2dif  13838  wrdsymb0  13896  wrdlenge2n0  13899  ccatsymb  13931  swrdnd2  14012  swrdnd0  14014  pfxnd  14044  pfxccat1  14059  swrdpfx  14064  pfxpfx  14065  wrd2ind  14080  pfxccatin12  14090  pfxccat3  14091  swrdccat  14092  pfxccatpfx1  14093  pfxccatpfx2  14094  swrdccatin1d  14100  pfxccatin12d  14102  repswswrd  14141  cshwidxmod  14160  s2f1o  14273  f1oun2prg  14274  wwlktovfo  14317  relexpreld  14394  relexpfld  14403  rtrclreclem3  14414  resqrex  14605  cau3lem  14709  reusq0  14817  rlimcld2  14930  climcn2  14944  isercoll  15019  climsup  15021  caurcvgr  15025  sumeq2ii  15045  summolem3  15066  zsum  15070  fsumadd  15091  fsum2dlem  15120  fsum0diag2  15133  fsummulc2  15134  fsumabs  15151  fsumrelem  15157  fsumrlim  15161  fsumo1  15162  o1fsum  15163  fsumiun  15171  qshash  15177  prodeq2ii  15262  prodmolem3  15282  fprodmul  15309  fproddiv  15310  fprod2dlem  15329  fprodsplit1f  15339  sin02gt0  15540  efieq1re  15547  p1modz1  15609  dvdsleabs2  15657  4dvdseven  15717  sumeven  15731  sumodd  15732  divalglem9  15745  smupvallem  15825  rppwr  15901  algfx  15917  eucalgcvga  15923  lcmfunsnlem1  15974  lcmfunsnlem2lem1  15975  lcmflefac  15985  qredeq  15994  fermltl  16114  modprm0  16135  pythagtriplem4  16149  pythagtriplem6  16151  pythagtriplem7  16152  pythagtriplem12  16156  pythagtriplem13  16157  pythagtriplem14  16158  pythagtriplem16  16160  difsqpwdvds  16216  pcmpt  16221  prmreclem2  16246  4sqlem11  16284  vdwlem9  16318  vdwlem11  16320  vdwlem12  16321  0ram  16349  0ram2  16350  0ramcl  16352  ramcl  16358  prmolelcmf  16377  cshwsidrepsw  16422  cshwshashlem2  16425  prmlem1  16436  prmlem2  16448  strfvd  16523  strfv2d  16524  strssd  16528  firest  16701  prdsdsval3  16753  imasbas  16780  imasds  16781  imasaddfnlem  16796  imasaddvallem  16797  imasvscafn  16805  qusaddvallem  16819  qusaddflem  16820  qusaddval  16821  qusaddf  16822  qusmulval  16823  qusmulf  16824  catideu  16941  idinv  17054  brcici  17065  invfuc  17239  2initoinv  17265  initoeu1w  17267  initoeu2lem0  17268  2termoinv  17272  termoeu1w  17274  mod2ile  17711  lubss  17726  acsmapd  17783  lidrididd  17875  gsumval2a  17890  mndind  17987  submefmnd  18055  mgm2nsgrplem4  18081  qusgrp2  18212  mulgnegnn  18233  pgrpsubgsymg  18532  fvcosymgeq  18552  gsmsymgreqlem1  18553  psgnunilem4  18620  pgpssslw  18734  sylow2alem2  18738  fislw  18745  efgsres  18859  rinvmod  18925  gsumval3lem2  19022  gsumzaddlem  19037  gsum2d  19088  nn0gsumfz  19100  telgsums  19109  dprddomcld  19119  ablfac2  19207  srgi  19257  ringi  19309  qusring2  19369  lssintcl  19732  lbsextlem3  19928  lbsextlem4  19929  zringlpirlem3  20182  psgnodpm  20280  psgndiflemB  20292  frlmup4  20493  lindff1  20512  lindfrn  20513  lmisfree  20534  evlseu  20758  mptcoe1fsupp  20847  cply1coe0bi  20932  mpfpf1  20978  pf1mpf  20979  mat0dimscm  21077  mdetdiagid  21208  mdet1  21209  mdetunilem9  21228  slesolinv  21288  cramerimp  21294  cpmatmcllem  21326  mptcoe1matfsupp  21410  mp2pm2mp  21419  chpdmat  21449  cctop  21614  subbascn  21862  cnss2  21885  cmpcovf  21999  2ndcctbss  22063  2ndcomap  22066  2ndcsep  22067  comppfsc  22140  ptclsg  22223  dfac14  22226  txcnp  22228  ptcnplem  22229  uptx  22233  txtube  22248  tx2ndc  22259  xkococnlem  22267  elqtop  22305  qtoprest  22325  indishmph  22406  ptcmpfi  22421  kqhmph  22427  csdfil  22502  filssufilg  22519  ufilen  22538  rnelfm  22561  fmfnfmlem4  22565  alexsubALTlem4  22658  ptcmplem4  22663  cnextfvval  22673  cnextcn  22675  cnextfres  22677  tmdgsum2  22704  imasf1oxmet  22985  metss  23118  met2ndci  23132  prdsxmslem2  23139  metust  23168  cfilucfil  23169  metustbl  23176  psmetutop  23177  opnreen  23439  rectbntr0  23440  fsumcn  23478  rescncf  23505  xrhmeo  23554  cnllycmp  23564  lebnumlem1  23569  lebnumlem3  23571  cfilss  23877  iscmet3lem1  23898  iscmet3lem2  23899  ivthicc  24065  ovolsslem  24091  ovoliunlem2  24110  ovoliunnul  24114  ovolicc2lem4  24127  voliunlem3  24159  volsup  24163  uniiccdif  24185  uniioombllem2  24190  volivth  24214  mbfimaopnlem  24262  mbflimsup  24273  i1fd  24288  itg1addlem4  24306  itg2addlem  24365  itg2gt0  24367  limciun  24500  dvadd  24546  dvmul  24547  dvco  24553  dvrec  24561  dvcnv  24583  dvferm  24594  rollelem  24595  dvlip  24599  dvlip2  24601  c1liplem1  24602  c1lip2  24604  dvgt0lem1  24608  dvivthlem1  24614  lhop1lem  24619  dvcnvrelem1  24623  dvcnvrelem2  24624  dvcvx  24626  dvfsumle  24627  dvfsumabs  24629  dvfsumlem1  24632  dvfsumlem2  24633  dvfsumlem4  24635  dvfsumrlim2  24638  dvfsum2  24640  ftc1cn  24649  ftc2ditglem  24651  itgsubstlem  24654  itgpowd  24656  tdeglem4  24664  mdegaddle  24678  mdegmullem  24682  deg1sublt  24714  ply1divmo  24739  fta1g  24771  dgrub  24834  dgrnznn  24847  dgradd2  24868  dvply1  24883  plyrem  24904  aalioulem4  24934  aalioulem5  24935  aalioulem6  24936  aaliou2  24939  taylf  24959  ulmdv  25001  psercn2  25021  abelth  25039  abelth2  25040  reeff1olem  25044  efopn  25252  logreclem  25351  isosctrlem2  25408  xrlimcnp  25557  basellem4  25672  ppiwordi  25750  musum  25779  chpub  25807  gausslemma2dlem0c  25945  2sqlem6  26010  addsqnreup  26030  2sqreulem1  26033  2sqreunnlem1  26036  dchrisumlema  26075  dchrisumlem2  26077  dchrisumlem3  26078  pntlemp  26197  pntleml  26198  ostth3  26225  iscgrglt  26311  colline  26446  axlowdimlem16  26754  axlowdimlem17  26755  axcontlem3  26763  axcontlem10  26770  uhgr2edg  27001  nbupgruvtxres  27200  cusgrres  27241  cusgrfilem2  27249  vdumgr0  27273  frusgrnn0  27364  wlklenvclwlkOLD  27448  wlkp1lem8  27473  pthdivtx  27521  upgrwlkdvde  27529  spthonepeq  27544  usgr2pthlem  27555  lfgrn1cycl  27594  wwlknbp1  27633  wwlknllvtx  27635  wlkiswwlks2lem3  27660  umgr2adedgspth  27737  clwlkclwwlklem3  27789  clwwisshclwwslemlem  27801  clwwisshclwws  27803  clwwlkel  27834  wwlksubclwwlk  27846  eleclclwwlknlem1  27848  eleclclwwlknlem2  27849  erclwwlknref  27857  clwwlknonccat  27884  clwwlknonex2lem2  27896  3wlkdlem4  27950  vdn0conngrumgrv2  27984  eucrctshift  28031  frgrnbnb  28081  frgrncvvdeqlem2  28088  frgrncvvdeqlem3  28089  fusgreghash2wspv  28123  numclwwlk2lem1  28164  numclwlk2lem2f  28165  numclwwlk5  28176  numclwwlk7  28179  frgrreggt1  28181  minvecolem4b  28664  minvecolem4  28666  bcsiALT  28965  ococin  29194  spanpr  29366  pjorthi  29455  nmbdoplbi  29810  nmcoplbi  29814  nmbdfnlbi  29835  nmcfnlbi  29838  nmopcoi  29881  branmfn  29891  hstnmoc  30009  mdsl0  30096  atomli  30168  atcvat4i  30183  atabsi  30187  foresf1o  30276  rabfodom  30277  abrexdomjm  30278  elpreq  30305  ifeqeqx  30312  disjiunel  30362  fovcld  30402  aciunf1lem  30428  ffsrn  30494  xlt2addrd  30511  supxrnemnf  30522  ssnnssfz  30539  dvdszzq  30560  resspos  30675  resstos  30676  gsummptres2  30741  archirngz  30871  orngsqr  30931  isarchiofld  30944  elrspunidl  31017  prmidl2  31024  qsidomlem2  31037  ssmxidl  31050  locfinreflem  31193  cmpcref  31203  fmcncfil  31282  xrge0iifiso  31286  elzdif0  31329  qqhval2lem  31330  esumcst  31430  esumrnmpt2  31435  esumpinfval  31440  esumpinfsum  31444  sigaclci  31499  insiga  31504  ldgenpisys  31533  measres  31589  measdivcstALTV  31592  dya2iocnrect  31647  dya2iocnei  31648  omssubadd  31666  carsggect  31684  carsgclctunlem2  31685  sitgclg  31708  eulerpartlemsv2  31724  eulerpartlemv  31730  eulerpartlemf  31736  eulerpartlemgh  31744  eulerpartlemgs2  31746  ballotlemfp1  31857  ballotlemfrcn0  31895  ftc2re  31977  fdvposlt  31978  fdvposle  31980  bnj1379  32210  bnj580  32293  bnj944  32318  bnj999  32338  bnj1204  32392  bnj1398  32414  cusgredgex  32476  pthacycspth  32512  derangenlem  32526  subfacp1lem3  32537  subfacp1lem5  32539  resconn  32601  cvmliftlem3  32642  satfv0fvfmla0  32768  satfv1fvfmla1  32778  mrsub0  32871  frpomin  33186  frrlem4  33234  frrlem8  33238  frrlem10  33240  fprlem1  33245  fprlem2  33246  frrlem15  33250  frrlem16  33251  sltres  33277  noextenddif  33283  nolesgn2ores  33287  nosep1o  33294  nosepeq  33297  nolt02o  33307  noresle  33308  nosupno  33311  nosupres  33315  nosupbnd1lem1  33316  nosupbnd1lem4  33319  nosupbnd1  33322  nosupbnd2lem1  33323  nosupbnd2  33324  sslttr  33376  cgrextend  33577  segconeq  33579  trisegint  33597  fwddifnp1  33734  ivthALT  33791  fnessref  33813  refssfne  33814  neibastop1  33815  filnetlem4  33837  ontgval  33887  unblimceq0lem  33953  unbdqndv2lem2  33957  unbdqndv2  33958  bj-babygodel  34045  bj-alrimd  34061  bj-exlimd  34066  bj-spcimdv  34330  bj-spcimdvv  34331  bj-finsumval0  34695  bj-fvimacnv0  34696  dfgcd3  34733  relowlssretop  34775  relowlpssretop  34776  onsucuni3  34779  finxpreclem4  34806  poimirlem18  35068  poimirlem21  35071  poimirlem25  35075  ftc1cnnclem  35121  ftc1cnnc  35122  ftc2nc  35132  dvasin  35134  dvacos  35135  abrexdom  35161  indexdom  35165  mettrifi  35188  equivtotbnd  35209  totbndbnd  35220  prdstotbnd  35225  heibor1lem  35240  bfplem1  35253  bfplem2  35254  opidonOLD  35283  rngodm1dm2  35363  zerdivemp1x  35378  equid1  36188  omllaw5N  36536  cmtcomlemN  36537  cmtbr3N  36543  omlfh3N  36548  atlen0  36599  exatleN  36693  hlrelat3  36701  cvrexchlem  36708  atlelt  36727  cvrat4  36732  4atlem11b  36897  4atlem12b  36900  lneq2at  37067  cdlema1N  37080  cdlemblem  37082  paddss12  37108  paddasslem2  37110  paddasslem4  37112  paddasslem6  37114  paddasslem12  37120  paddunN  37216  poml4N  37242  poml5N  37243  osumcllem6N  37250  pexmidlem6N  37264  pl42lem2N  37269  ltrnu  37410  ltrneq2  37437  trlval2  37452  cdlemd6  37492  cdleme25b  37643  cdleme29b  37664  cdlemefr29exN  37691  ltrniotacnvval  37871  cdlemk28-3  38197  dochexmidlem7  38755  muldvds2d  39280  frlmsnic  39440  mzpsubmpt  39671  mzpsubst  39676  eqrabdioph  39705  rabdiophlem2  39730  elpell14qr2  39790  elpell1qr2  39800  pellfundre  39809  pellfundge  39810  pellfundglb  39813  pellfund14gap  39815  congabseq  39902  jm2.22  39923  jm2.23  39924  jm2.26lem3  39929  wepwsolem  39973  dnwech  39979  aomclem2  39986  aomclem4  39988  pwfi2f1o  40027  ss2iundf  40347  dssmapf1od  40709  neik0pk1imk0  40737  gneispace  40824  grur1cld  40927  cpcolld  40953  mnuop23d  40961  mnuprdlem1  40967  mnuprdlem2  40968  mnurndlem1  40976  grumnudlem  40980  radcnvrat  41005  sbiota1  41125  ordelordALT  41230  2pm13.193  41245  ee11an  41383  refsumcn  41646  rfcnnnub  41652  disjxp1  41690  xrnmnfpnf  41706  ssinc  41710  nssd  41728  ralimda  41761  disjf1o  41805  disjinfi  41807  choicefi  41816  axccdom  41840  dmrelrnrel  41843  monoords  41916  fperiodmullem  41922  xadd0ge  41939  xrssre  41967  xrlexaddrp  41971  xrred  41984  infxr  41986  fiminre2  41997  xrnpnfmnf  42101  monoordxrv  42108  monoord2xrv  42110  fsumsplit1  42201  fsumiunss  42204  fmul01  42209  fmuldfeqlem1  42211  fmuldfeq  42212  fmul01lt1lem1  42213  fmul01lt1lem2  42214  cncfmptss  42216  climinf  42235  climsuselem1  42236  climsuse  42237  limcperiod  42257  limcrecl  42258  sumnnodd  42259  limcleqr  42273  0ellimcdiv  42278  climleltrp  42305  limsuppnfdlem  42330  limsupresxr  42395  liminfresxr  42396  liminfvalxr  42412  cnrefiisplem  42458  xlimmnfvlem1  42461  xlimpnfvlem1  42465  cncfperiod  42508  icccncfext  42516  cncfiooicclem1  42522  dvbdfbdioolem1  42557  dvnmptdivc  42567  dvdsn1add  42568  dvnmptconst  42570  dvnmul  42572  dvmptfprodlem  42573  dvmptfprod  42574  dvnprodlem2  42576  iblspltprt  42602  itgsubsticclem  42604  itgspltprt  42608  itgsbtaddcnst  42611  stoweidlem3  42632  stoweidlem16  42645  stoweidlem17  42646  stoweidlem19  42648  stoweidlem20  42649  stoweidlem23  42652  stoweidlem25  42654  stoweidlem27  42656  stoweidlem31  42660  stoweidlem34  42663  stoweidlem42  42671  stoweidlem48  42677  stoweidlem51  42680  stoweidlem52  42681  stoweidlem59  42688  wallispilem1  42694  wallispilem3  42696  stirlinglem13  42715  fourierdlem16  42752  fourierdlem20  42756  fourierdlem21  42757  fourierdlem38  42774  fourierdlem42  42778  fourierdlem46  42781  fourierdlem48  42783  fourierdlem49  42784  fourierdlem50  42785  fourierdlem54  42789  fourierdlem68  42803  fourierdlem72  42807  fourierdlem73  42808  fourierdlem76  42811  fourierdlem79  42814  fourierdlem81  42816  fourierdlem86  42821  fourierdlem89  42824  fourierdlem90  42825  fourierdlem91  42826  fourierdlem92  42827  fourierdlem97  42832  fourierdlem101  42836  fourierdlem103  42838  fourierdlem104  42839  fourierdlem111  42846  etransclem24  42887  etransclem25  42888  etransclem28  42891  etransclem41  42904  etransclem44  42907  etransclem48  42911  salexct  42961  dfsalgen2  42968  sge0f1o  43008  sge0rnbnd  43019  sge0split  43035  sge0iunmptlemre  43041  sge0fodjrnlem  43042  sge0iunmpt  43044  nnfoctbdjlem  43081  iundjiunlem  43085  meadjiunlem  43091  ismeannd  43093  meaiuninclem  43106  omeiunle  43143  carageniuncllem1  43147  caratheodorylem1  43152  hoidmvlelem4  43224  hoiqssbllem2  43249  salpreimagelt  43330  salpreimalegt  43332  pimdecfgtioc  43337  smfaddlem2  43384  smflimlem6  43396  nsssmfmbflem  43398  smfpimcclem  43425  or2expropbilem1  43611  funressndmfvrn  43623  2leaddle2  43842  smonoord  43875  uniimaprimaeqfv  43886  fundcmpsurbijinjpreimafv  43911  fundcmpsurinjALT  43916  iccpartf  43935  ich2exprop  43975  ichnreuop  43976  ichreuopeq  43977  sprbisymrel  44003  fmtnodvds  44048  proththdlem  44118  gbowgt5  44267  gboge9  44269  gbege6  44270  stgoldbwt  44281  sbgoldbalt  44286  bgoldbnnsum3prm  44309  isomgrtrlem  44343  uspgrbisymrelALT  44370  ssnn0ssfz  44738  ldepspr  44869  iunord  45193  bnd2d  45198  setrecsss  45217
  Copyright terms: Public domain W3C validator