Theorem syld 48

Description: Syllogism deduction. Deduction associated with syl 18. See conventions 30688 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

Step	Hyp	Ref	Expression
1		syld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syld.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
3	2	a1d 26	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpdd 44	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  49  3syld  61  sylsyld  62  nsyld  157  pm2.61d  181  sylibd  242  sylbid  243  sylibrd  262  sylbird  263  syland  614  animpimp2impd  859  ax12v2  2221  alrimdd  2256  axc16g  2302  axc16nf  2305  axc11r  2406  sb4a  2518  2eu1  2684  2eu1v  2685  ss2ralv  4016  ss2rexv  4017  trel3  5228  poss  5569  sess2  5625  wefrc  5653  wereu2  5656  predtrss  6321  frpomin  6339  ordpss  6387  funun  6580  ssimaex  6964  f1cofveqaeq  7253  f1imass  7260  soisoi  7324  isores3  7331  isofrlem  7336  isoselem  7337  weniso  7350  abnexg  7751  oninton  7790  orduniorsuc  7822  limuni3  7844  tfindsg  7853  limom  7874  resf1extb  7927  f1o2ndf1  8113  soxp  8121  xpord3inddlem  8146  soseq  8151  extmptsuppeq  8180  smoel  8343  tfrlem9  8368  tz7.49  8428  seqomlem1  8433  odi  8560  omass  8561  omeulem2  8564  oeordsuc  8576  oeeulem  8583  naddsuc2  8684  ertr  8706  swoord2  8724  ecopovtrn  8814  domtriord  9107  pssnn  9149  unxpdomlem2  9213  isinf  9221  f1finf1o  9229  findcard3  9239  frfi  9241  unblem3  9250  supssd  9419  infssd  9450  en3lplem1  9577  inf3lem5  9597  cantnfle  9636  cantnfp1lem3  9645  ttrcltr  9681  frmin  9717  rankxpsuc  9850  tcrank  9852  ficardom  9943  carduni  9963  infxpenlem  9993  dfac8alem  10009  ac10ct  10014  ween  10015  alephdom  10061  alephle  10068  iscard3  10073  alephfp  10088  pwsdompw  10182  infdif  10187  cfslbn  10247  cofsmo  10249  cfcof  10254  fin1a2s  10394  domtriomlem  10422  ac6num  10459  zorn2lem3  10478  axdclem2  10500  imadomg  10514  iundom2g  10520  ficard  10545  fpwwe2lem7  10618  fpwwe2  10624  gchpwdom  10651  gchaclem  10659  tskr1om2  10749  inar1  10756  tskord  10761  tskuni  10764  grudomon  10798  grur1a  10800  grur1  10801  addnidpi  10882  ltexnq  10956  genpnnp  10986  addclprlem2  10998  mulclprlem  11000  psslinpr  11012  ltexprlem6  11022  ltexprlem7  11023  addcanpr  11027  mulgt0sr  11086  map2psrpr  11091  supsrlem  11092  axrrecex  11144  letr  11300  dedekind  11369  recex  11842  lemul12b  12068  fimaxre2  12156  lbreu  12161  nnrecgt0  12275  nnunb  12496  bndndx  12499  zeo  12678  uzind  12684  fzind  12690  fnn0ind  12691  suprfinzcl  12706  suprzcl2  12958  zmax  12965  rpnnen1lem5  13001  xrletr  13179  qbtwnre  13221  qsqueeze  13223  qextltlem  13224  xralrple  13227  xlesubadd  13285  supxrunb1  13341  icoshft  13496  zltaddlt1le  13528  fzen  13565  elfz0fzfz0  13657  elfzmlbp  13663  elfzo0z  13726  fzofzim  13734  fzo1fzo0n0  13740  elfzodifsumelfzo  13756  ssfzoulel  13785  modadd1  13937  modmul1  13956  uzrdgfni  13990  fsuppmapnn0fiub0  14025  fsuppmapnn0ub  14027  fsuppmapnn0fz  14028  seqf1olem1  14073  seqf1olem2  14074  expnbnd  14264  faclbnd4lem4  14328  hashgt23el  14457  seqcoll  14497  hashle2pr  14510  elss2prb  14521  ccatalpha  14627  swrdsbslen  14698  swrdspsleq  14699  swrdswrdlem  14737  swrdswrd  14738  pfxccatin12lem2a  14760  pfxccatin12lem1  14761  pfxccatin12lem3  14765  swrdccat3blem  14772  reuccatpfxs1lem  14779  repswswrd  14817  cshf1  14843  swrd2lsw  14985  sqeqd  15213  sqrmo  15298  cau3lem  15402  icodiamlt  15485  limsupbnd2  15530  lo1bdd2  15571  climuni  15599  rlimcn3  15637  mulcn2  15643  o1of2  15660  rlimo1  15664  lo1le  15699  iseralt  15732  cvgrat  15933  fprodss  15998  rpnnen2lem12  16277  ruclem3  16285  sqrt2irr  16301  p1modz1  16313  dvdsmodexp  16314  dvds2lem  16322  dvdslelem  16363  dvdsabseq  16367  divalglem8  16454  bitsinv1lem  16495  sadcaddlem  16511  smu01lem  16539  smueqlem  16544  bezoutlem4  16596  dfgcd2  16600  algcvga  16633  lcmfunsnlem1  16691  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  lcmfdvdsb  16697  coprmgcdb  16703  coprmdvds2  16708  coprmprod  16715  isprm3  16737  prmdvdsfz  16760  isprm5  16762  coprm  16766  rpexp12i  16779  phibndlem  16825  dfphi2  16829  eulerthlem2  16837  odzdvds  16851  iserodd  16891  pclem  16894  pcpremul  16899  pcqcl  16912  pcdvdsb  16925  pcprmpw2  16938  difsqpwdvds  16943  pcaddlem  16944  pcmptcl  16947  pcfac  16955  prmpwdvds  16960  unbenlem  16964  prmreclem1  16972  4sqlem17  17017  vdwmc2  17035  vdwlem9  17045  vdwlem10  17046  vdwlem13  17049  vdwnnlem3  17053  ramcl  17085  prmgaplem7  17113  mreiincl  17644  initoid  18054  termoid  18055  initoeu2lem1  18067  pospo  18395  resspos  18481  resstos  18482  dirge  18655  cyccom  19270  gsmsymgrfixlem1  19493  oddvdsnn0  19610  oddvds  19613  odcl2  19631  gexdvds  19650  sylow2alem2  19684  sylow2a  19685  efgi2  19791  efgsrel  19800  efgs1b  19802  imasabl  19942  cyggex2  19963  telgsums  20059  pgpfac1lem2  20143  pgpfac1lem3a  20144  pgpfac1lem3  20145  pgpfac1lem5  20147  zrtermorngc  20724  zrtermoringc  20756  lmodfopnelem2  20994  lssssr  21049  rnglidlmcl  21315  unichnlidl  21336  gzrngunitlem  21547  znunit  21678  frgpcyg  21688  lsmcss  21807  obselocv  21843  obslbs  21845  mhpvarcl  22276  cply1mul  22421  gsummoncoe1  22433  cpmatacl  22838  cpmatinvcl  22839  cpmatmcllem  22840  m2cpminvid2lem  22876  mp2pm2mplem4  22931  pm2mp  22947  chfacfisf  22976  chfacfisfcpmat  22977  chfacfscmul0  22980  chfacfpmmul0  22984  cayhamlem4  23010  ordtrest2lem  23325  leordtval2  23334  lecldbas  23341  cncls  23396  cncnp  23402  cnpresti  23410  lmcnp  23426  cnt0  23468  isreg2  23499  cmpsublem  23521  cmpsub  23522  tgcmp  23523  bwth  23532  dfconn2  23541  1stcfb  23567  1stcelcls  23583  islly2  23606  dislly  23619  reftr  23636  comppfsc  23654  kgencn2  23679  txcnp  23742  txindis  23756  txcmplem1  23763  txlm  23770  xkohaus  23775  cnmptcom  23800  kqfvima  23852  isr0  23859  fgss2  23996  fbasrn  24006  filuni  24007  ufilmax  24029  isufil2  24030  cfinufil  24050  fmfnfmlem1  24076  fmfnfmlem2  24077  fmfnfmlem4  24079  fmfnfm  24080  fmco  24083  flimopn  24097  hausflim  24103  flimrest  24105  fclsopn  24136  flimfnfcls  24150  alexsubALTlem2  24170  alexsubALTlem3  24171  alexsubALT  24173  ptcmplem2  24175  cnextcn  24189  symgtgp  24228  qustgplem  24243  tsmsres  24266  tsmsxplem1  24275  isucn2  24400  imasdsf1olem  24495  bldisj  24520  blssps  24546  blss  24547  metcnp3  24662  ngptgp  24758  nrginvrcn  24814  nmoleub  24853  xrsmopn  24935  icccmplem3  24947  reconnlem2  24950  rectbntr0  24955  rescncf  25021  iocopnst  25064  iccpnfcnv  25068  lebnumii  25090  nmoleub2lem  25238  nmhmcn  25244  iscfil3  25397  iscau2  25401  iscau3  25402  iscau4  25403  iscmet3lem2  25416  caussi  25421  equivcfil  25423  equivcau  25424  ivthlem2  25576  ivthlem3  25577  ovoliunlem2  25627  ovoliunnul  25631  ioombl1lem4  25685  dyadmax  25722  dyadmbl  25724  volsup2  25729  itg2le  25863  itg2const2  25865  itg2seq  25866  itgsplitioo  25962  rolle  26114  c1lip1  26121  dvivthlem1  26132  lhop1  26138  dvcnvrelem1  26141  dvfsumrlim  26155  ply1divmo  26258  ig1peu  26297  plypf1  26334  coeaddlem  26371  dvply2g  26411  fta1  26434  quotcan  26435  aalioulem4  26461  ulmcaulem  26519  ulmcn  26524  pilem2  26577  sincosq1lem  26624  sinq12gt0  26634  sinq12ge0  26635  tanord1  26664  lognegb  26717  logrec  26890  logbgcd1irr  26921  dcubic  26973  xrlimcnp  27095  o1cxp  27101  ftalem2  27200  ftalem3  27201  fsumdvdscom  27311  chtub  27338  vmasum  27342  bcmono  27403  bposlem3  27412  bposlem7  27416  lgsdir  27458  lgsqrlem2  27473  lgsqrmodndvds  27479  gausslemma2dlem6  27498  gausslemma2d  27500  lgsquadlem2  27507  2lgslem3a1  27526  2lgslem3b1  27527  2lgslem3c1  27528  2lgslem3d1  27529  2sqlem6  27549  2sq2  27559  2sqmod  27562  dchrisumlem3  27617  pntrsumbnd2  27693  pntpbnd1  27712  pntibnd  27719  pntlem3  27735  pntleml  27737  ltsres  27788  nosepon  27791  nolesgn2o  27797  nogesgn1o  27799  nodenselem8  27817  nosupbnd1lem1  27834  madess  28021  madebdaylemlrcut  28054  peano5uzs  28559  bdayfinbndlem1  28622  z12bday  28640  brbtwn2  29192  colinearalg  29197  axcontlem10  29260  edgupgr  29421  edglnl  29430  usgruspgrb  29470  subupgr  29574  uhgrspan1  29590  usgredgsscusgredg  29746  fusgrn0degnn0  29786  upgrewlkle2  29893  uspgr2wlkeq  29932  redwlk  29957  wlkdlem2  29968  upgrwlkdvdelem  30022  pthdlem1  30052  pthdlem2  30054  crctcshwlkn0lem3  30098  wlkiswwlks1  30153  wwlksm1edg  30167  wwlksnred  30178  wwlksnextbi  30180  umgr2adedgspth  30234  clwlkclwwlklem2fv2  30284  clwlkclwwlklem2a  30286  clwlkclwwlkf1lem3  30294  clwwisshclwwslemlem  30301  clwwlkf  30335  clwwlkext2edg  30344  wwlksubclwwlk  30346  clwwlknonex2lem2  30396  eupth2lems  30526  frgrwopreglem4a  30598  frgrregorufrg  30614  ex-natded5.3-2  30696  isgrpo  30786  vacn  30983  ubthlem2  31160  htthlem  31206  normgt0  31416  shmodsi  31678  spansneleq  31859  h1datomi  31870  nmcexi  32315  pjnormssi  32457  stm1add3i  32536  golem2  32561  cvnsym  32579  dmdmd  32589  mdslmd1lem1  32614  mdslmd1i  32618  mdexchi  32624  atcveq0  32637  superpos  32643  hatomistici  32651  atoml2i  32672  atcvat2i  32676  chirredlem1  32679  atcvat3i  32685  mdsymlem3  32694  mdsymlem5  32696  cdj3lem2b  32726  cdj3i  32730  submarchi  33443  dfufd2  33781  tpr2rico  34243  ordtrest2NEWlem  34253  xrge0iifcnv  34264  omssubadd  34631  eulerpartlemb  34699  ballotlemfc0  34824  ballotlemfcc  34825  ftc2re  34926  fissorduni  35419  fineqvinfep  35457  axsepg2  35472  axsepg4  35475  axpowg2  35479  axpowg3  35480  loop1cycl  35524  subfacp1lem6  35572  iccllysconn  35637  cvmfolem  35666  satfsschain  35751  satfrel  35754  satfdm  35756  sat1el2xp  35766  satffunlem1lem1  35789  dmopab3rexdif  35792  satffunlem2lem2  35793  satffun  35796  fundmpss  36154  dfon2lem3  36170  dfon2lem6  36173  axextbdist  36185  dfrdg4  36338  5segofs  36393  cgrextend  36395  segconeu  36398  btwncomim  36400  btwnswapid  36404  btwnintr  36406  btwnexch3  36407  btwndiff  36414  ifscgr  36431  cgrxfr  36442  btwnxfr  36443  lineext  36463  brofs2  36464  linecgr  36468  lineid  36470  idinside  36471  endofsegid  36472  btwnconn1lem13  36486  btwnconn3  36490  finminlem  36714  nn0prpwlem  36718  cldbnd  36722  clsint2  36725  fnessref  36753  neibastop3  36758  fgmin  36766  onsuct0  36837  limsucncmpi  36841  tr0elw  36880  tr0el  36881  bj-nnfea  37244  bj-axc14  37376  bj-restn0  37615  bj-0int  37626  wl-19.2reqv  38062  wl-aetr  38067  wl-axc11r  38068  fin2so  38141  tan2h  38146  lindsenlbs  38149  poimirlem2  38156  poimirlem9  38163  poimirlem17  38171  poimirlem18  38172  poimirlem21  38175  poimirlem23  38177  poimirlem26  38180  poimirlem29  38183  poimirlem30  38184  poimirlem31  38185  poimir  38187  heicant  38189  mblfinlem2  38192  mblfinlem3  38193  itg2addnclem  38205  itg2addnclem2  38206  itg2gt0cn  38209  ftc1anclem5  38231  ftc1anclem6  38232  filbcmb  38274  nninfnub  38285  mettrifi  38291  geomcau  38293  istotbnd3  38305  sstotbnd2  38308  ismtybndlem  38340  heibor1lem  38343  heiborlem1  38345  heiborlem8  38352  heiborlem10  38354  heibor  38355  opidonOLD  38386  riscer  38522  crngohomfo  38540  keridl  38566  ispridl2  38572  ispridlc  38604  ac6s6  38706  eqvreltr  39225  eldisjdmqsim  39351  suceldisj  39352  eldisjs6  39474  dral1-o  39563  ax12indalem  39604  ax12inda2ALT  39605  lsatcveq0  39691  eqlkr3  39760  atlatmstc  39978  atlrelat1  39980  hlrelat2  40062  intnatN  40066  cvrexchlem  40078  cvratlem  40080  cvrat2  40088  atltcvr  40094  cvrat3  40101  cvrat4  40102  ps-1  40136  ps-2  40137  lplnnle2at  40200  lvolnle3at  40241  2llnma3r  40447  cdlemblem  40452  pmapjoin  40511  elpcliN  40552  lhpmcvr4N  40685  4atexlemnclw  40729  trlnidatb  40836  cdlemc4  40853  cdlemd3  40859  cdleme3g  40893  cdleme7d  40905  cdleme11c  40920  cdleme11dN  40921  cdleme21b  40985  cdleme21c  40986  cdleme21i  40994  cdleme22b  41000  cdleme35fnpq  41108  cdlemf1  41220  trlord  41228  cdlemg6c  41279  dihglblem6  41999  dochlkr  42044  dochkrshp  42045  dihjat1lem  42087  dochexmidlem5  42123  dochexmidlem8  42126  qsalrel  42894  remulcand  43085  prjspner1  43245  fphpdo  43431  pellexlem5  43447  pellexlem6  43448  jm2.26lem3  43615  unxpwdom3  43709  omlimcl2  43856  oe0suclim  43891  cantnfresb  43938  tfsconcatb0  43958  naddgeoa  44008  iscard5  44149  sqrtcval  44254  ov2ssiunov2  44313  frege124d  44374  19.41rg  45146  relpfrlem  45549  modelaxreplem2  45575  stoweidlem34  46635  ormklocald  47477  evenwodadd  47490  cfsetsnfsetf1  47680  fcoresf1  47690  euoreqb  47730  2reu8i  47734  ralralimp  47899  f1oresf1o2  47912  zm1nn  47923  elfz2z  47936  2tceilhalfelfzo1  47957  m1modmmod  47985  modlt0b  47990  muldvdsfacgt  48007  muldvdsfacm1  48008  iccpartlt  48057  iccelpart  48066  icceuelpartlem  48068  fargshiftf1  48074  sprsymrelf1lem  48124  paireqne  48144  reuopreuprim  48159  goldbachthlem2  48182  odz2prm2pw  48199  fmtnoprmfac1lem  48200  fmtnofac2lem  48204  prmdvdsfmtnof1  48223  sfprmdvdsmersenne  48239  lighneallem2  48242  lighneallem4  48246  fppr2odd  48380  gbegt5  48410  gbowge7  48412  bgoldbtbndlem4  48457  bgoldbtbnd  48458  tgoldbach  48466  grimuhgr  48536  grimcnv  48537  grimco  48538  isuspgrim0  48543  isuspgrimlem  48544  upgrimwlklem5  48550  upgrimtrlslem2  48554  uhgrimisgrgriclem  48579  clnbgrgrimlem  48582  clnbgrgrim  48583  grimedg  48584  grtriprop  48590  isubgr3stgrlem3  48617  isubgr3stgrlem4  48618  isubgr3stgrlem6  48620  isubgr3stgrlem7  48621  uspgrlimlem3  48639  grlimedgclnbgr  48644  grlimgrtrilem2  48651  grlimgrtri  48652  grlicsym  48662  gpgedgvtx1  48711  gpgedgiov  48714  gpgedg2ov  48715  gpgedg2iv  48716  pgnioedg1  48757  pgnioedg2  48758  pgnioedg3  48759  pgnioedg4  48760  pgnioedg5  48761  pgnbgreunbgrlem2lem1  48763  pgnbgreunbgrlem2lem2  48764  pgnbgreunbgrlem2lem3  48765  pgnbgreunbgrlem5lem1  48769  pgnbgreunbgrlem5lem2  48770  pgnbgreunbgrlem5lem3  48771  lcosslsp  49098  lindslinindsimp1  49117  snlindsntor  49131  itcovalt2  49337  eenglngeehlnmlem2  49398  itsclc0yqsol  49424  itschlc0xyqsol1  49426  itschlc0xyqsol  49427  opnneilv  49567  i0oii  49578  io1ii  49579  iscnrm3lem4  49594  iscnrm3r  49606  setrec1lem4  50348  aacllem  50470