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

Theorem syld 44
 Description: Syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.) Notice that syld 44 has the same form as syl 16 with added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 22 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible.
Hypotheses
Ref Expression
syld.1
syld.2
Assertion
Ref Expression
syld

Proof of Theorem syld
StepHypRef Expression
1 syld.1 . 2
2 syld.2 . . 3
32a1d 25 . 2
41, 3mpdd 40 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4 This theorem is referenced by:  3syld  55  sylsyld  56  nsyld  140  pm2.61d  158  sylibd  214  sylbid  215  sylibrd  234  sylbird  235  syland  481  a2andOLD  812  ax12v  1855  alrimdd  1880  axc112  1937  nfeqf2  2041  equveliOLD  2089  sbequi  2116  dral1-o  2233  ax12indalem  2275  ax12inda2ALT  2276  2eu1  2376  axext3  2437  trel3  4553  poss  4807  sess2  4853  wefrc  4878  wereu2  4881  funun  5635  ssimaex  5938  f1imass  6172  soisoi  6224  isores3  6231  isofrlem  6236  isoselem  6237  weniso  6250  oninton  6635  orduniorsuc  6665  limuni3  6687  tfindsg  6695  limom  6715  f1o2ndf1  6908  soxp  6913  extmptsuppeq  6943  smoel  7050  smogt  7057  tfrlem9  7073  tz7.49  7129  seqomlem1  7134  odi  7247  omass  7248  omeulem2  7251  oeordsuc  7262  oeeulem  7269  ertr  7345  swoord2  7360  ecopovtrn  7433  domtriord  7683  onomeneq  7727  unxpdomlem2  7745  isinf  7753  pssnn  7758  findcard3  7783  frfi  7785  unblem3  7794  dffi3  7911  en3lplem1  8052  inf3lem3  8068  inf3lem5  8070  noinfep  8097  cantnfle  8111  cantnfp1lem3  8120  cantnfleOLD  8141  cantnfp1lem3OLD  8146  rankxpsuc  8321  tcrank  8323  ficardom  8363  carduni  8383  infxpenlem  8412  dfac8alem  8431  ac10ct  8436  ween  8437  alephdom  8483  alephle  8490  iscard3  8495  alephfp  8510  cdainf  8593  pwsdompw  8605  infdif  8610  cfslbn  8668  cofsmo  8670  cfsmolem  8671  cfcof  8675  fin1a2s  8815  domtriomlem  8843  ac6num  8880  zorn2lem3  8899  axdclem2  8921  imadomg  8933  iundom2g  8936  ficard  8961  fpwwe2lem8  9036  fpwwe2  9042  gchaclem  9077  tskr1om2  9167  inar1  9174  tskord  9179  tskuni  9182  grudomon  9216  grur1a  9218  grur1  9219  addnidpi  9300  ltexnq  9374  genpnnp  9404  addclprlem2  9416  mulclprlem  9418  psslinpr  9430  ltaddpr2  9434  ltexprlem6  9440  ltexprlem7  9441  addcanpr  9445  mulgt0sr  9503  map2psrpr  9508  supsrlem  9509  axrrecex  9561  letr  9699  dedekind  9765  recex  10206  lemul12b  10424  mulgt1  10426  ledivmulOLD  10444  fimaxre2  10516  lbreu  10518  nnrecgt0  10598  nnunb  10816  bndndx  10819  zeo  10973  uzind  10979  fzind  10987  fnn0ind  10988  suprfinzcl  11003  suprzcl2  11201  zmax  11208  rpnnen1lem5  11241  xrletr  11390  qbtwnre  11427  qsqueeze  11429  qextltlem  11430  xralrple  11433  xlesubadd  11484  supxrunb1  11540  icoshft  11671  fzen  11732  elfz1b  11777  elfz0fzfz0  11808  elfzmlbmOLD  11814  elfzmlbp  11815  fzo1fzo0n0  11864  elfzo0z  11865  fzofzim  11869  elfzodifsumelfzo  11882  ssfzoulel  11906  modadd1  12033  modmul1  12040  uzrdgfni  12069  fsuppmapnn0fiub0  12099  fsuppmapnn0ub  12101  fsuppmapnn0fz  12102  seqcl2  12125  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqf1olem1  12146  seqf1olem2  12147  seqid2  12153  seqhomo  12154  expnbnd  12295  faclbnd4lem4  12374  seqcoll  12512  swrdnd  12657  swrdvalodm2  12664  swrdswrdlem  12684  swrdswrd  12685  reuccats1lem  12705  swrdccatin12lem2a  12710  swrdccatin12lem2b  12711  swrdccatin12lem3  12715  swrdccat3a  12719  swrdccat3blem  12720  repswswrd  12756  swrd2lsw  12890  sqeqd  12999  sqrmo  13085  cau3lem  13187  limsupbnd2  13306  lo1bdd2  13347  climuni  13375  rlimcn2  13413  mulcn2  13418  o1of2  13435  rlimo1  13439  lo1le  13474  isercolllem1  13487  iseralt  13507  cvgrat  13692  fprodss  13755  rpnnen2  13959  ruclem3  13966  sqrt2irr  13982  dvds2lem  13996  dvdslelem  14030  divalglem8  14058  bitsinv1lem  14091  sadcaddlem  14107  smu01lem  14135  smueqlem  14140  bezoutlem4  14179  algcvga  14208  isprm3  14226  coprm  14241  coprmdvds2  14244  isprm5  14253  rpexp12i  14263  phibndlem  14300  dfphi2  14304  eulerthlem2  14312  odzdvds  14322  iserodd  14359  pclem  14362  pcpremul  14367  pcqcl  14380  pcdvdsb  14392  pcprmpw2  14405  pcaddlem  14407  pcmptcl  14410  pcfac  14418  prmpwdvds  14422  unbenlem  14426  prmreclem1  14434  4sqlem17  14479  vdwmc2  14497  vdwlem9  14507  vdwlem10  14508  vdwlem13  14511  vdwnnlem3  14515  ramcl  14547  mreiincl  14993  pospo  15603  dirge  15867  gsmsymgrfixlem1  16452  oddvdsnn0  16568  oddvds  16571  odcl2  16587  gexdvds  16604  sylow1lem1  16618  sylow2alem2  16638  sylow2a  16639  efgi2  16743  efgsrel  16752  efgs1b  16754  cyggex2  16899  telgsums  17022  pgpfac1lem2  17126  pgpfac1lem3a  17127  pgpfac1lem3  17128  pgpfac1lem5  17130  lssssr  17599  cply1mul  18335  gsummoncoe1  18346  gzrngunitlem  18482  znunit  18602  frgpcyg  18612  lsmcss  18723  obselocv  18759  obslbs  18761  scmataddcl  19018  scmatsubcl  19019  cpmatacl  19217  cpmatinvcl  19218  cpmatmcllem  19219  m2cpminvid2lem  19255  mp2pm2mplem4  19310  pm2mp  19326  chfacfisf  19355  chfacfisfcpmat  19356  chfacfscmul0  19359  chfacfpmmul0  19363  cayhamlem4  19389  ordtrest2lem  19704  leordtval2  19713  lecldbas  19720  cncls  19775  cncnp  19781  cnpresti  19789  lmcnp  19805  cnt0  19847  isreg2  19878  cmpsublem  19899  cmpsub  19900  tgcmp  19901  bwth  19910  bwthOLD  19911  dfcon2  19920  1stcfb  19946  2ndcctbss  19956  1stcelcls  19962  islly2  19985  dislly  19998  reftr  20015  comppfsc  20033  kgencn2  20058  txcnp  20121  txindis  20135  txcmplem1  20142  txlm  20149  xkohaus  20154  cnmptcom  20179  kqfvima  20231  isr0  20238  fgss2  20375  fbasrn  20385  filuni  20386  ufilmax  20408  isufil2  20409  cfinufil  20429  fmfnfmlem1  20455  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  fmco  20462  flimopn  20476  hausflim  20482  flimrest  20484  fclsopn  20515  flimfnfcls  20529  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALT  20551  ptcmplem2  20553  cnextcn  20567  symgtgp  20600  qustgplem  20619  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  isucn2  20782  imasdsf1olem  20876  bldisj  20901  blssps  20927  blss  20928  metcnp3  21043  ngptgp  21150  nrginvrcn  21200  nmoleub  21238  xrsmopn  21317  icccmplem3  21329  reconnlem2  21332  rectbntr0  21337  rescncf  21401  iocopnst  21440  iccpnfcnv  21444  lebnumii  21466  nmoleub2lem  21597  nmhmcn  21603  fgcfil  21710  iscfil3  21712  iscau2  21716  iscau3  21717  iscau4  21718  iscmet3lem2  21731  cfilres  21735  caussi  21736  equivcfil  21738  equivcau  21739  ivthlem2  21864  ivthlem3  21865  ovoliunlem2  21914  ovoliunnul  21918  ovolicc2lem3  21930  ioombl1lem4  21971  dyadmax  22007  dyadmbl  22009  volsup2  22014  itg2le  22146  itg2const2  22148  itg2seq  22149  itgsplitioo  22244  dvnres  22334  rolle  22391  c1lip1  22398  dvivthlem1  22409  lhop1  22415  dvcnvrelem1  22418  dvfsumrlim  22432  ply1divmo  22536  ig1peu  22572  plypf1  22609  coeaddlem  22646  fta1  22704  quotcan  22705  aalioulem4  22731  ulmcaulem  22789  ulmcn  22794  pilem2  22847  sincosq1lem  22890  sinq12gt0  22900  sinq12ge0  22901  sineq0  22914  tanord1  22924  lognegb  22974  logrec  23151  dcubic  23177  xrlimcnp  23298  o1cxp  23304  ftalem2  23347  ftalem3  23348  fsumdvdscom  23461  chtub  23487  vmasum  23491  bcmono  23552  bposlem3  23561  bposlem7  23565  lgsdir  23605  lgsqrlem2  23617  lgsdchr  23623  lgsquadlem2  23630  2sqlem6  23644  dchrisumlem3  23676  pntrsumbnd2  23752  pntpbnd1  23771  pntibnd  23778  pntlem3  23794  pntleml  23796  brbtwn2  24208  colinearalg  24213  axcontlem10  24276  redwlk  24608  usgra2adedgspthlem2  24612  fargshiftf1  24637  constr3trllem2  24651  4cycl4dv  24667  usg2wlkeq  24708  wwlknred  24723  wwlknextbi  24725  wwlkm1edg  24735  clwlkswlks  24758  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkf  24794  clwwlkext2edg  24802  wwlksubclwwlk  24804  clwwisshclwwlem1  24805  usg2wotspth  24884  vdusgra0nedg  24908  usgravd0nedg  24918  usgravd00  24919  eupath2  24980  frgraregorufrg  25072  numclwwlkovf2ex  25086  numclwlk1lem2foa  25091  numclwlk1lem2fo  25095  ex-natded5.3-2  25129  isgrpo  25198  opidonOLD  25324  vacn  25604  ubthlem2  25787  htthlem  25834  normgt0  26044  shmodsi  26307  spansneleq  26488  h1datomi  26499  pjjsi  26618  nmcexi  26945  pjnormssi  27087  stm1add3i  27166  golem2  27191  cvnsym  27209  dmdmd  27219  mdslmd1lem1  27244  mdslmd1i  27248  mdexchi  27254  atcveq0  27267  superpos  27273  hatomistici  27281  atoml2i  27302  atcvat2i  27306  chirredlem1  27309  atcvat3i  27315  mdsymlem3  27324  mdsymlem5  27326  cdj3lem2b  27356  cdj3i  27360  supssd  27527  2sqmod  27636  resspos  27647  resstos  27648  submarchi  27730  tpr2rico  27894  ordtrest2NEWlem  27904  xrge0iifcnv  27915  eulerpartlemb  28307  ballotlemfc0  28431  ballotlemfcc  28432  subfacp1lem6  28629  iccllyscon  28695  cvmfolem  28724  cvmliftlem7  28736  cvmliftlem10  28739  ghomf1olem  29034  fundmpss  29196  dfon2lem3  29217  dfon2lem6  29220  axext4dist  29233  setlikess  29275  trpredtr  29313  trpredmintr  29314  dftrpred3g  29316  trpredrec  29321  frmin  29322  soseq  29334  wfrlem12  29354  frrlem5e  29395  frrlem11  29399  sltval2  29416  sltres  29424  nodenselem4  29444  nodenselem8  29448  nobndlem6  29457  dfrdg4  29600  5segofs  29656  cgrextend  29658  segconeu  29661  btwncomim  29663  btwnswapid  29667  btwnintr  29669  btwnexch3  29670  btwndiff  29677  ifscgr  29694  cgrxfr  29705  btwnxfr  29706  lineext  29726  brofs2  29727  linecgr  29731  lineid  29733  idinside  29734  endofsegid  29735  btwnconn1lem13  29749  btwnconn3  29753  onsuct0  29906  limsucncmpi  29910  wl-aetr  29983  fin2so  30040  tan2h  30047  heicant  30049  mblfinlem2  30052  mblfinlem3  30053  itg2addnclem  30066  itg2addnclem2  30067  itg2gt0cn  30070  ftc1anclem5  30094  ftc1anclem6  30095  finminlem  30136  nn0prpwlem  30140  cldbnd  30144  clsint2  30147  fnessref  30175  neibastop3  30180  fgmin  30188  filbcmb  30231  nninfnub  30244  mettrifi  30250  geomcau  30252  istotbnd3  30267  sstotbnd2  30270  ismtybndlem  30302  heibor1lem  30305  heiborlem1  30307  heiborlem8  30314  heiborlem10  30316  heibor  30317  riscer  30391  crngohomfo  30403  keridl  30429  ispridl2  30435  ispridlc  30467  ac6s6  30580  fphpdo  30751  icodiamlt  30756  pellexlem5  30769  pellexlem6  30770  jm2.26lem3  30943  dfac21  31012  unxpwdom3  31041  ordpss  31360  stoweidlem34  31816  ralralimp  32295  zm1nn  32325  ltsubnn0  32327  elfz2z  32331  usgedgimp  32403  usgvincvad  32404  usgedgimpALT  32406  usgvincvadALT  32407  initoid  32611  termoid  32612  initoeu1  32617  initoeu2lem1  32620  termoeu1  32624  zrtermorngc  32809  zrtermoringc  32878  ztprmneprm  32936  lcosslsp  33039  lindslinindsimp1  33058  lindslinindsimp2lem5  33063  snlindsntor  33072  aacllem  33216  19.41rg  33323  bj-exalimi  34225  lsatcveq0  34757  eqlkr3  34826  atlatmstc  35044  atlrelat1  35046  hlrelat2  35127  intnatN  35131  cvrexchlem  35143  cvratlem  35145  cvrat2  35153  atltcvr  35159  cvrat3  35166  cvrat4  35167  ps-1  35201  ps-2  35202  lplnnle2at  35265  lvolnle3at  35306  2llnma3r  35512  cdlemblem  35517  pmapjoin  35576  elpcliN  35617  lhpmcvr4N  35750  4atexlemnclw  35794  trlnidatb  35902  cdlemc4  35919  cdlemd3  35925  cdleme3g  35959  cdleme7d  35971  cdleme11c  35986  cdleme11dN  35987  cdleme21b  36052  cdleme21c  36053  cdleme21i  36061  cdleme22b  36067  cdleme35fnpq  36175  cdlemf1  36287  trlord  36295  cdlemg6c  36346  dihglblem6  37067  dochlkr  37112  dochkrshp  37113  dihjat1lem  37155  dochexmidlem5  37191  dochexmidlem8  37194 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
 Copyright terms: Public domain W3C validator