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

Theorem syld 47
Description: Syllogism deduction. Deduction associated with syl 17. See conventions 27582 for the meaning of "associated deduction" or "deduction form". (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
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 43 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:  syldc  48  3syld  60  sylsyld  61  nsyld  155  pm2.61d  171  sylibd  230  sylbid  231  sylibrd  250  sylbird  251  syland  592  animpimp2impd  864  ax12v2  2215  alrimdd  2249  axc16g  2310  axc16nf  2313  axc11rvOLD  2316  axc11r  2360  alrimddOLD  2368  nfeqf2OLD  2464  sbequi  2533  2eu1  2714  axext3  2783  trel3  4947  poss  5228  sess2  5274  wefrc  5299  wereu2  5302  funun  6140  ssimaex  6478  f1cofveqaeq  6733  f1imass  6739  soisoi  6796  isores3  6803  isofrlem  6808  isoselem  6809  weniso  6822  abnexg  7188  oninton  7224  orduniorsuc  7254  limuni3  7276  tfindsg  7284  limom  7304  f1o2ndf1  7513  soxp  7518  extmptsuppeq  7547  smoel  7687  tfrlem9  7711  tz7.49  7770  seqomlem1  7775  odi  7890  omass  7891  omeulem2  7894  oeordsuc  7905  oeeulem  7912  ertr  7988  swoord2  8005  ecopovtrn  8080  domtriord  8339  onomeneq  8383  unxpdomlem2  8398  isinf  8406  pssnn  8411  findcard3  8436  frfi  8438  unblem3  8447  dffi3  8570  en3lplem1  8748  inf3lem5  8770  cantnfle  8809  cantnfp1lem3  8818  rankxpsuc  8986  tcrank  8988  ficardom  9064  carduni  9084  infxpenlem  9113  dfac8alem  9129  ac10ct  9134  ween  9135  alephdom  9181  alephle  9188  iscard3  9193  alephfp  9208  cdainf  9293  pwsdompw  9305  infdif  9310  cfslbn  9368  cofsmo  9370  cfcof  9375  fin1a2s  9515  domtriomlem  9543  ac6num  9580  zorn2lem3  9599  axdclem2  9621  imadomg  9635  iundom2g  9641  ficard  9666  fpwwe2lem8  9738  fpwwe2  9744  gchaclem  9779  tskr1om2  9869  inar1  9876  tskord  9881  tskuni  9884  grudomon  9918  grur1a  9920  grur1  9921  addnidpi  10002  ltexnq  10076  genpnnp  10106  addclprlem2  10118  mulclprlem  10120  psslinpr  10132  ltexprlem6  10142  ltexprlem7  10143  addcanpr  10147  mulgt0sr  10205  map2psrpr  10210  supsrlem  10211  axrrecex  10263  letr  10410  dedekind  10479  recex  10938  lemul12b  11159  mulgt1  11161  fimaxre2  11248  lbreu  11252  nnrecgt0  11338  nnunb  11549  bndndx  11552  zeo  11723  uzind  11729  fzind  11735  fnn0ind  11736  suprfinzcl  11752  suprzcl2  11991  zmax  11998  rpnnen1lem5  12031  xrletr  12201  qbtwnre  12242  qsqueeze  12244  qextltlem  12245  xralrple  12248  xlesubadd  12305  supxrunb1  12361  icoshft  12509  zltaddlt1le  12541  fzen  12575  elfz0fzfz0  12662  elfzmlbp  12668  elfzo0z  12728  fzofzim  12733  fzo1fzo0n0  12737  elfzodifsumelfzo  12752  ssfzoulel  12780  modadd1  12925  modmul1  12941  uzrdgfni  12975  fsuppmapnn0fiub0  13010  fsuppmapnn0ub  13012  fsuppmapnn0fz  13013  seqf1olem1  13057  seqf1olem2  13058  expnbnd  13210  faclbnd4lem4  13297  seqcoll  13459  hashle2pr  13470  elss2prb  13480  ccatalpha  13584  swrdsbslen  13666  swrdspsleq  13667  swrdswrdlem  13677  swrdswrd  13678  reuccats1lem  13697  swrdccatin12lem2a  13703  swrdccatin12lem2b  13704  swrdccatin12lem3  13708  swrdccat3a  13712  swrdccat3blem  13713  repswswrd  13749  cshf1  13774  swrd2lsw  13914  sqeqd  14123  sqrmo  14209  cau3lem  14311  icodiamlt  14391  limsupbnd2  14431  lo1bdd2  14472  climuni  14500  rlimcn2  14538  mulcn2  14543  o1of2  14560  rlimo1  14564  lo1le  14599  isercolllem1  14612  iseralt  14632  cvgrat  14830  fprodss  14893  znnenlemOLD  15154  rpnnen2lem12  15168  ruclem3  15176  sqrt2irr  15193  p1modz1  15204  dvdsmodexp  15205  dvds2lem  15211  dvdslelem  15248  dvdsabseq  15252  divalglem8  15337  bitsinv1lem  15376  sadcaddlem  15392  smu01lem  15420  smueqlem  15425  bezoutlem4  15472  dfgcd2  15476  algcvga  15505  lcmfunsnlem1  15563  lcmfunsnlem2lem1  15564  lcmfunsnlem2lem2  15565  lcmfdvdsb  15569  coprmgcdb  15575  coprmdvds2  15580  coprmprod  15587  isprm3  15608  prmdvdsfz  15628  isprm5  15630  coprm  15634  rpexp12i  15645  phibndlem  15686  dfphi2  15690  eulerthlem2  15698  odzdvds  15711  iserodd  15751  pclem  15754  pcpremul  15759  pcqcl  15772  pcdvdsb  15784  pcprmpw2  15797  difsqpwdvds  15802  pcaddlem  15803  pcmptcl  15806  pcfac  15814  prmpwdvds  15819  unbenlem  15823  prmreclem1  15831  4sqlem17  15876  vdwmc2  15894  vdwlem9  15904  vdwlem10  15905  vdwlem13  15908  vdwnnlem3  15912  ramcl  15944  prmgaplem7  15972  mreiincl  16455  initoid  16853  termoid  16854  initoeu2lem1  16862  pospo  17172  dirge  17436  gsmsymgrfixlem1  18042  oddvdsnn0  18158  oddvds  18161  odcl2  18177  gexdvds  18194  sylow2alem2  18228  sylow2a  18229  efgi2  18333  efgsrel  18342  efgs1b  18344  cyggex2  18493  telgsums  18586  pgpfac1lem2  18670  pgpfac1lem3a  18671  pgpfac1lem3  18672  pgpfac1lem5  18674  lmodfopnelem2  19098  lssssr  19153  lssssrOLD  19154  cply1mul  19866  gsummoncoe1  19876  gzrngunitlem  20013  znunit  20113  frgpcyg  20123  lsmcss  20240  obselocv  20276  obslbs  20278  cpmatacl  20728  cpmatinvcl  20729  cpmatmcllem  20730  m2cpminvid2lem  20766  mp2pm2mplem4  20821  pm2mp  20837  chfacfisf  20866  chfacfisfcpmat  20867  chfacfscmul0  20870  chfacfpmmul0  20874  cayhamlem4  20900  ordtrest2lem  21215  leordtval2  21224  lecldbas  21231  cncls  21286  cncnp  21292  cnpresti  21300  lmcnp  21316  cnt0  21358  isreg2  21389  cmpsublem  21410  cmpsub  21411  tgcmp  21412  bwth  21421  dfconn2  21430  1stcfb  21456  1stcelcls  21472  islly2  21495  dislly  21508  reftr  21525  comppfsc  21543  kgencn2  21568  txcnp  21631  txindis  21645  txcmplem1  21652  txlm  21659  xkohaus  21664  cnmptcom  21689  kqfvima  21741  isr0  21748  fgss2  21885  fbasrn  21895  filuni  21896  ufilmax  21918  isufil2  21919  cfinufil  21939  fmfnfmlem1  21965  fmfnfmlem2  21966  fmfnfmlem4  21968  fmfnfm  21969  fmco  21972  flimopn  21986  hausflim  21992  flimrest  21994  fclsopn  22025  flimfnfcls  22039  alexsubALTlem2  22059  alexsubALTlem3  22060  alexsubALT  22062  ptcmplem2  22064  cnextcn  22078  symgtgp  22112  qustgplem  22131  tsmsres  22154  tsmsxplem1  22163  isucn2  22290  imasdsf1olem  22385  bldisj  22410  blssps  22436  blss  22437  metcnp3  22552  ngptgp  22647  nrginvrcn  22703  nmoleub  22742  xrsmopn  22822  icccmplem3  22834  reconnlem2  22837  rectbntr0  22842  rescncf  22907  iocopnst  22946  iccpnfcnv  22950  lebnumii  22972  nmoleub2lem  23120  nmhmcn  23126  iscfil3  23277  iscau2  23281  iscau3  23282  iscau4  23283  iscmet3lem2  23296  cfilres  23300  caussi  23301  equivcfil  23303  equivcau  23304  ivthlem2  23427  ivthlem3  23428  ovoliunlem2  23478  ovoliunnul  23482  ioombl1lem4  23536  dyadmax  23573  dyadmbl  23575  volsup2  23580  itg2le  23714  itg2const2  23716  itg2seq  23717  itgsplitioo  23812  rolle  23961  c1lip1  23968  dvivthlem1  23979  lhop1  23985  dvcnvrelem1  23988  dvfsumrlim  24002  ply1divmo  24103  ig1peu  24139  plypf1  24176  coeaddlem  24213  fta1  24271  quotcan  24272  aalioulem4  24298  ulmcaulem  24356  ulmcn  24361  pilem2  24414  sincosq1lem  24458  sinq12gt0  24468  sinq12ge0  24469  tanord1  24492  lognegb  24544  logrec  24709  dcubic  24781  xrlimcnp  24903  o1cxp  24909  ftalem2  25008  ftalem3  25009  fsumdvdscom  25119  chtub  25145  vmasum  25149  bcmono  25210  bposlem3  25219  bposlem7  25223  lgsdir  25265  lgsqrlem2  25280  lgsqrmodndvds  25286  lgsdchr  25288  gausslemma2dlem6  25305  gausslemma2d  25307  lgsquadlem2  25314  2lgslem3a1  25333  2lgslem3b1  25334  2lgslem3c1  25335  2lgslem3d1  25336  2sqlem6  25356  dchrisumlem3  25388  pntrsumbnd2  25464  pntpbnd1  25483  pntibnd  25490  pntlem3  25506  pntleml  25508  brbtwn2  25993  colinearalg  25998  axcontlem10  26061  edgupgr  26237  edglnl  26247  usgruspgrb  26285  subupgr  26389  uhgrspan1  26405  usgredgsscusgredg  26577  fusgrn0degnn0  26617  upgrewlkle2  26724  uspgr2wlkeq  26764  redwlk  26791  wlkdlem2  26802  upgrwlkdvdelem  26854  pthdlem1  26884  pthdlem2  26886  crctcshwlkn0lem3  26927  wlkiswwlks1  26988  wwlksm1edg  27002  wwlksnred  27023  wwlksnextbi  27025  umgr2adedgspth  27082  clwlkclwwlklem2fv2  27133  clwlkclwwlklem2a  27135  clwlkclwwlkf1lem3  27143  clwwisshclwwslemlem  27150  clwwlkf  27190  clwwlkext2edg  27200  wwlksubclwwlk  27203  clwwlknonwwlknonbOLD  27269  clwwlknonex2lem2  27271  eupth2lems  27405  frgrwopreglem4a  27479  frgrregorufrg  27495  ex-natded5.3-2  27590  isgrpo  27674  vacn  27871  ubthlem2  28049  htthlem  28096  normgt0  28306  shmodsi  28570  spansneleq  28751  h1datomi  28762  nmcexi  29207  pjnormssi  29349  stm1add3i  29428  golem2  29453  cvnsym  29471  dmdmd  29481  mdslmd1lem1  29506  mdslmd1i  29510  mdexchi  29516  atcveq0  29529  superpos  29535  hatomistici  29543  atoml2i  29564  atcvat2i  29568  chirredlem1  29571  atcvat3i  29577  mdsymlem3  29586  mdsymlem5  29588  cdj3lem2b  29618  cdj3i  29622  supssd  29808  infssd  29809  2sqmod  29967  resspos  29978  resstos  29979  submarchi  30059  tpr2rico  30277  ordtrest2NEWlem  30287  xrge0iifcnv  30298  omssubadd  30681  eulerpartlemb  30749  ballotlemfc0  30873  ballotlemfcc  30874  ftc2re  30995  subfacp1lem6  31484  iccllysconn  31549  cvmfolem  31578  fundmpss  31980  dfon2lem3  32004  dfon2lem6  32007  axext4dist  32020  trpredtr  32044  trpredmintr  32045  dftrpred3g  32047  trpredrec  32052  frpomin  32053  frmin  32057  soseq  32069  frrlem5e  32103  sltres  32130  nosepon  32133  nolesgn2o  32139  nodenselem8  32156  nosupbnd1lem1  32169  dfrdg4  32373  5segofs  32428  cgrextend  32430  segconeu  32433  btwncomim  32435  btwnswapid  32439  btwnintr  32441  btwnexch3  32442  btwndiff  32449  ifscgr  32466  cgrxfr  32477  btwnxfr  32478  lineext  32498  brofs2  32499  linecgr  32503  lineid  32505  idinside  32506  endofsegid  32507  btwnconn1lem13  32521  btwnconn3  32525  finminlem  32627  nn0prpwlem  32632  cldbnd  32636  clsint2  32639  fnessref  32667  neibastop3  32672  fgmin  32680  onsuct0  32751  limsucncmpi  32755  bj-axc14  33145  bj-restn0  33348  bj-0int  33360  wl-19.2reqv  33619  wl-aetr  33625  fin2so  33703  tan2h  33708  lindsenlbs  33711  poimirlem2  33718  poimirlem9  33725  poimirlem17  33733  poimirlem18  33734  poimirlem21  33737  poimirlem23  33739  poimirlem26  33742  poimirlem29  33745  poimirlem30  33746  poimirlem31  33747  poimir  33749  heicant  33751  mblfinlem2  33754  mblfinlem3  33755  itg2addnclem  33767  itg2addnclem2  33768  itg2gt0cn  33771  ftc1anclem5  33795  ftc1anclem6  33796  filbcmb  33841  nninfnub  33852  mettrifi  33858  geomcau  33860  istotbnd3  33875  sstotbnd2  33878  ismtybndlem  33910  heibor1lem  33913  heiborlem1  33915  heiborlem8  33922  heiborlem10  33924  heibor  33925  opidonOLD  33956  riscer  34092  crngohomfo  34110  keridl  34136  ispridl2  34142  ispridlc  34174  ac6s6  34284  dral1-o  34677  ax12indalem  34718  ax12inda2ALT  34719  lsatcveq0  34806  eqlkr3  34875  atlatmstc  35093  atlrelat1  35095  hlrelat2  35177  intnatN  35181  cvrexchlem  35193  cvratlem  35195  cvrat2  35203  atltcvr  35209  cvrat3  35216  cvrat4  35217  ps-1  35251  ps-2  35252  lplnnle2at  35315  lvolnle3at  35356  2llnma3r  35562  cdlemblem  35567  pmapjoin  35626  elpcliN  35667  lhpmcvr4N  35800  4atexlemnclw  35844  trlnidatb  35952  cdlemc4  35969  cdlemd3  35975  cdleme3g  36009  cdleme7d  36021  cdleme11c  36036  cdleme11dN  36037  cdleme21b  36101  cdleme21c  36102  cdleme21i  36110  cdleme22b  36116  cdleme35fnpq  36224  cdlemf1  36336  trlord  36344  cdlemg6c  36395  dihglblem6  37115  dochlkr  37160  dochkrshp  37161  dihjat1lem  37203  dochexmidlem5  37239  dochexmidlem8  37242  fphpdo  37877  pellexlem5  37893  pellexlem6  37894  jm2.26lem3  38063  unxpwdom3  38160  ov2ssiunov2  38486  frege124d  38547  ordpss  39147  19.41rg  39258  stoweidlem34  40724  ralralimp  41862  f1oresf1o2  41875  zm1nn  41886  elfz2z  41894  iccpartlt  41929  iccelpart  41938  icceuelpartlem  41940  fargshiftf1  41946  pfxccatin12lem1  41992  reuccatpfxs1lem  42002  goldbachthlem2  42027  odz2prm2pw  42044  fmtnoprmfac1lem  42045  fmtnofac2lem  42049  prmdvdsfmtnof1  42068  sfprmdvdsmersenne  42089  lighneallem2  42092  lighneallem4  42096  gbegt5  42218  gbowge7  42220  bgoldbtbndlem4  42265  bgoldbtbnd  42266  tgoldbach  42274  sprsymrelf1lem  42303  zrtermorngc  42563  zrtermoringc  42632  lcosslsp  42789  lindslinindsimp1  42808  snlindsntor  42822  m1modmmod  42878  setrec1lem4  42999  aacllem  43112
  Copyright terms: Public domain W3C validator