Theorem syld 48

Description: Syllogism deduction. Deduction associated with syl 18. See conventions 30751 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  2215  alrimdd  2250  axc16g  2296  axc16nf  2299  axc11r  2400  sb4a  2512  2eu1  2678  2eu1v  2679  ss2ralv  4008  ss2rexv  4009  trel3  5227  poss  5571  sess2  5627  wefrc  5655  wereu2  5658  predtrss  6323  frpomin  6341  ordpss  6389  funun  6582  ssimaex  6966  f1cofveqaeq  7255  f1imass  7262  soisoi  7326  isores3  7333  isofrlem  7338  isoselem  7339  weniso  7352  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  10246  cofsmo  10248  cfcof  10253  fin1a2s  10393  domtriomlem  10421  ac6num  10458  zorn2lem3  10477  axdclem2  10499  imadomg  10513  iundom2g  10519  ficard  10544  fpwwe2lem7  10617  fpwwe2  10623  gchpwdom  10650  gchaclem  10658  tskr1om2  10748  inar1  10755  tskord  10760  tskuni  10763  grudomon  10797  grur1a  10799  grur1  10800  addnidpi  10881  ltexnq  10955  genpnnp  10985  addclprlem2  10997  mulclprlem  10999  psslinpr  11011  ltexprlem6  11021  ltexprlem7  11022  addcanpr  11026  mulgt0sr  11085  map2psrpr  11090  supsrlem  11091  axrrecex  11143  letr  11299  dedekind  11368  recex  11841  lemul12b  12067  fimaxre2  12155  lbreu  12160  nnrecgt0  12274  nnunb  12495  bndndx  12498  zeo  12677  uzind  12683  fzind  12689  fnn0ind  12690  suprfinzcl  12705  suprzcl2  12957  zmax  12964  rpnnen1lem5  13000  xrletr  13178  qbtwnre  13220  qsqueeze  13222  qextltlem  13223  xralrple  13226  xlesubadd  13284  supxrunb1  13340  icoshft  13495  zltaddlt1le  13527  fzen  13564  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  16276  ruclem3  16284  sqrt2irr  16300  p1modz1  16312  dvdsmodexp  16313  dvds2lem  16321  dvdslelem  16362  dvdsabseq  16366  divalglem8  16453  bitsinv1lem  16494  sadcaddlem  16510  smu01lem  16538  smueqlem  16543  bezoutlem4  16595  dfgcd2  16599  algcvga  16632  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfdvdsb  16696  coprmgcdb  16702  coprmdvds2  16707  coprmprod  16714  isprm3  16736  prmdvdsfz  16759  isprm5  16761  coprm  16765  rpexp12i  16778  phibndlem  16824  dfphi2  16828  eulerthlem2  16836  odzdvds  16850  iserodd  16890  pclem  16893  pcpremul  16898  pcqcl  16911  pcdvdsb  16924  pcprmpw2  16937  difsqpwdvds  16942  pcaddlem  16943  pcmptcl  16946  pcfac  16954  prmpwdvds  16959  unbenlem  16963  prmreclem1  16971  4sqlem17  17016  vdwmc2  17034  vdwlem9  17044  vdwlem10  17045  vdwlem13  17048  vdwnnlem3  17052  ramcl  17084  prmgaplem7  17112  mreiincl  17643  initoid  18053  termoid  18054  initoeu2lem1  18066  pospo  18394  resspos  18480  resstos  18481  dirge  18654  cyccom  19269  gsmsymgrfixlem1  19492  oddvdsnn0  19609  oddvds  19612  odcl2  19630  gexdvds  19649  sylow2alem2  19683  sylow2a  19684  efgi2  19790  efgsrel  19799  efgs1b  19801  imasabl  19941  cyggex2  19962  telgsums  20058  pgpfac1lem2  20142  pgpfac1lem3a  20143  pgpfac1lem3  20144  pgpfac1lem5  20146  crngrhmfo  20574  zrtermorngc  20742  zrtermoringc  20774  lmodfopnelem2  21020  lssssr  21075  rnglidlmcl  21341  unichnlidl  21362  gzrngunitlem  21582  znunit  21713  frgpcyg  21723  lsmcss  21842  obselocv  21878  obslbs  21880  mhpvarcl  22311  cply1mul  22456  gsummoncoe1  22468  cpmatacl  22873  cpmatinvcl  22874  cpmatmcllem  22875  m2cpminvid2lem  22911  mp2pm2mplem4  22966  pm2mp  22982  chfacfisf  23011  chfacfisfcpmat  23012  chfacfscmul0  23015  chfacfpmmul0  23019  cayhamlem4  23045  ordtrest2lem  23360  leordtval2  23369  lecldbas  23376  cncls  23431  cncnp  23437  cnpresti  23445  lmcnp  23461  cnt0  23503  isreg2  23534  cmpsublem  23556  cmpsub  23557  tgcmp  23558  bwth  23567  dfconn2  23576  1stcfb  23602  1stcelcls  23618  islly2  23641  dislly  23654  reftr  23671  comppfsc  23689  kgencn2  23714  txcnp  23777  txindis  23791  txcmplem1  23798  txlm  23805  xkohaus  23810  cnmptcom  23835  kqfvima  23887  isr0  23894  fgss2  24031  fbasrn  24041  filuni  24042  ufilmax  24064  isufil2  24065  cfinufil  24085  fmfnfmlem1  24111  fmfnfmlem2  24112  fmfnfmlem4  24114  fmfnfm  24115  fmco  24118  flimopn  24132  hausflim  24138  flimrest  24140  fclsopn  24171  flimfnfcls  24185  alexsubALTlem2  24205  alexsubALTlem3  24206  alexsubALT  24208  ptcmplem2  24210  cnextcn  24224  symgtgp  24263  qustgplem  24278  tsmsres  24301  tsmsxplem1  24310  isucn2  24435  imasdsf1olem  24530  bldisj  24555  blssps  24581  blss  24582  metcnp3  24697  ngptgp  24793  nrginvrcn  24849  nmoleub  24888  xrsmopn  24970  icccmplem3  24982  reconnlem2  24985  rectbntr0  24990  rescncf  25056  iocopnst  25099  iccpnfcnv  25103  lebnumii  25125  nmoleub2lem  25273  nmhmcn  25279  iscfil3  25432  iscau2  25436  iscau3  25437  iscau4  25438  iscmet3lem2  25451  caussi  25456  equivcfil  25458  equivcau  25459  ivthlem2  25611  ivthlem3  25612  ovoliunlem2  25662  ovoliunnul  25666  ioombl1lem4  25720  dyadmax  25757  dyadmbl  25759  volsup2  25764  itg2le  25898  itg2const2  25900  itg2seq  25901  itgsplitioo  25997  rolle  26149  c1lip1  26156  dvivthlem1  26167  lhop1  26173  dvcnvrelem1  26176  dvfsumrlim  26190  ply1divmo  26293  ig1peu  26332  plypf1  26369  coeaddlem  26406  dvply2g  26446  fta1  26469  quotcan  26470  aalioulem4  26498  ulmcaulem  26557  ulmcn  26562  pilem2  26615  sincosq1lem  26662  sinq12gt0  26672  sinq12ge0  26673  tanord1  26702  lognegb  26755  logrec  26928  logbgcd1irr  26959  dcubic  27011  xrlimcnp  27133  o1cxp  27139  ftalem2  27238  ftalem3  27239  fsumdvdscom  27349  chtub  27376  vmasum  27380  bcmono  27441  bposlem3  27450  bposlem7  27454  lgsdir  27496  lgsqrlem2  27511  lgsqrmodndvds  27517  gausslemma2dlem6  27536  gausslemma2d  27538  lgsquadlem2  27545  2lgslem3a1  27564  2lgslem3b1  27565  2lgslem3c1  27566  2lgslem3d1  27567  2sqlem6  27587  2sq2  27597  2sqmod  27600  dchrisumlem3  27655  pntrsumbnd2  27731  pntpbnd1  27750  pntibnd  27757  pntlem3  27773  pntleml  27775  ltsres  27826  nosepon  27829  nolesgn2o  27835  nogesgn1o  27837  nodenselem8  27855  nosupbnd1lem1  27872  madess  28059  madebdaylemlrcut  28092  peano5uzs  28597  bdayfinbndlem1  28660  z12bday  28678  brbtwn2  29255  colinearalg  29260  axcontlem10  29323  edgupgr  29484  edglnl  29493  usgruspgrb  29533  subupgr  29637  uhgrspan1  29653  usgredgsscusgredg  29809  fusgrn0degnn0  29849  upgrewlkle2  29956  uspgr2wlkeq  29995  redwlk  30020  wlkdlem2  30031  upgrwlkdvdelem  30085  pthdlem1  30115  pthdlem2  30117  crctcshwlkn0lem3  30161  wlkiswwlks1  30216  wwlksm1edg  30230  wwlksnred  30241  wwlksnextbi  30243  umgr2adedgspth  30297  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a  30349  clwlkclwwlkf1lem3  30357  clwwisshclwwslemlem  30364  clwwlkf  30398  clwwlkext2edg  30407  wwlksubclwwlk  30409  clwwlknonex2lem2  30459  eupth2lems  30589  frgrwopreglem4a  30661  frgrregorufrg  30677  ex-natded5.3-2  30759  isgrpo  30849  vacn  31046  ubthlem2  31223  htthlem  31269  normgt0  31479  shmodsi  31741  spansneleq  31922  h1datomi  31933  nmcexi  32378  pjnormssi  32520  stm1add3i  32599  golem2  32624  cvnsym  32642  dmdmd  32652  mdslmd1lem1  32677  mdslmd1i  32681  mdexchi  32687  atcveq0  32700  superpos  32706  hatomistici  32714  atoml2i  32735  atcvat2i  32739  chirredlem1  32742  atcvat3i  32748  mdsymlem3  32757  mdsymlem5  32759  cdj3lem2b  32789  cdj3i  32793  submarchi  33506  dfufd2  33840  tpr2rico  34302  ordtrest2NEWlem  34312  xrge0iifcnv  34323  omssubadd  34690  eulerpartlemb  34758  ballotlemfc0  34883  ballotlemfcc  34884  ftc2re  34985  fissorduni  35480  fineqvinfep  35538  axsepg2  35553  axsepg4  35556  axpowg2  35560  axpowg3  35561  loop1cycl  35629  subfacp1lem6  35677  iccllysconn  35742  cvmfolem  35771  satfsschain  35856  satfrel  35859  satfdm  35861  sat1el2xp  35871  satffunlem1lem1  35894  dmopab3rexdif  35897  satffunlem2lem2  35898  satffun  35901  fundmpss  36259  dfon2lem3  36275  dfon2lem6  36278  axextbdist  36290  dfrdg4  36443  5segofs  36498  cgrextend  36500  segconeu  36503  btwncomim  36505  btwnswapid  36509  btwnintr  36511  btwnexch3  36512  btwndiff  36519  ifscgr  36536  cgrxfr  36547  btwnxfr  36548  lineext  36568  brofs2  36569  linecgr  36573  lineid  36575  idinside  36576  endofsegid  36577  btwnconn1lem13  36591  btwnconn3  36595  finminlem  36829  nn0prpwlem  36833  cldbnd  36837  clsint2  36840  fnessref  36868  neibastop3  36873  fgmin  36881  onsuct0  36952  limsucncmpi  36956  tr0elw  36995  tr0el  36996  bj-nnfea  37359  bj-axc14  37491  bj-restn0  37732  bj-0int  37743  wl-19.2reqv  38179  wl-aetr  38184  wl-axc11r  38185  fin2so  38258  tan2h  38263  lindsenlbs  38266  poimirlem2  38273  poimirlem9  38280  poimirlem17  38288  poimirlem18  38289  poimirlem21  38292  poimirlem23  38294  poimirlem26  38297  poimirlem29  38300  poimirlem30  38301  poimirlem31  38302  poimir  38304  heicant  38306  mblfinlem2  38309  mblfinlem3  38310  itg2addnclem  38322  itg2addnclem2  38323  itg2gt0cn  38326  ftc1anclem5  38348  ftc1anclem6  38349  filbcmb  38391  nninfnub  38402  mettrifi  38408  geomcau  38410  istotbnd3  38422  sstotbnd2  38425  ismtybndlem  38457  heibor1lem  38460  heiborlem1  38462  heiborlem8  38469  heiborlem10  38471  heibor  38472  opidonOLD  38503  riscer  38639  crngohomfo  38657  keridl  38683  ispridl2  38689  ispridlc  38721  ac6s6  38821  eqvreltr  39340  eldisjdmqsim  39466  suceldisj  39467  eldisjs6  39589  dral1-o  39678  ax12indalem  39719  ax12inda2ALT  39720  lsatcveq0  39806  eqlkr3  39875  atlatmstc  40093  atlrelat1  40095  hlrelat2  40177  intnatN  40181  cvrexchlem  40193  cvratlem  40195  cvrat2  40203  atltcvr  40209  cvrat3  40216  cvrat4  40217  ps-1  40251  ps-2  40252  lplnnle2at  40315  lvolnle3at  40356  2llnma3r  40562  cdlemblem  40567  pmapjoin  40626  elpcliN  40667  lhpmcvr4N  40800  4atexlemnclw  40844  trlnidatb  40951  cdlemc4  40968  cdlemd3  40974  cdleme3g  41008  cdleme7d  41020  cdleme11c  41035  cdleme11dN  41036  cdleme21b  41100  cdleme21c  41101  cdleme21i  41109  cdleme22b  41115  cdleme35fnpq  41223  cdlemf1  41335  trlord  41343  cdlemg6c  41394  dihglblem6  42114  dochlkr  42159  dochkrshp  42160  dihjat1lem  42202  dochexmidlem5  42238  dochexmidlem8  42241  qsalrel  43009  remulcand  43200  prjspner1  43358  fphpdo  43544  pellexlem5  43560  pellexlem6  43561  jm2.26lem3  43728  unxpwdom3  43822  omlimcl2  43969  oe0suclim  44004  cantnfresb  44051  tfsconcatb0  44071  naddgeoa  44121  iscard5  44262  sqrtcval  44367  ov2ssiunov2  44426  frege124d  44487  19.41rg  45259  relpfrlem  45662  modelaxreplem2  45688  stoweidlem34  46748  ormklocald  47590  evenwodadd  47602  cfsetsnfsetf1  47796  fcoresf1  47806  euoreqb  47846  2reu8i  47850  ralralimp  48015  f1oresf1o2  48028  zm1nn  48039  elfz2z  48052  2tceilhalfelfzo1  48073  m1modmmod  48101  modlt0b  48106  muldvdsfacgt  48123  muldvdsfacm1  48124  iccpartlt  48173  iccelpart  48182  icceuelpartlem  48184  fargshiftf1  48190  sprsymrelf1lem  48240  paireqne  48260  reuopreuprim  48275  goldbachthlem2  48298  odz2prm2pw  48315  fmtnoprmfac1lem  48316  fmtnofac2lem  48320  prmdvdsfmtnof1  48339  sfprmdvdsmersenne  48355  lighneallem2  48358  lighneallem4  48362  fppr2odd  48496  gbegt5  48526  gbowge7  48528  bgoldbtbndlem4  48573  bgoldbtbnd  48574  tgoldbach  48582  grimuhgr  48652  grimcnv  48653  grimco  48654  isuspgrim0  48659  isuspgrimlem  48660  upgrimwlklem5  48666  upgrimtrlslem2  48670  uhgrimisgrgriclem  48695  clnbgrgrimlem  48698  clnbgrgrim  48699  grimedg  48700  grtriprop  48706  isubgr3stgrlem3  48733  isubgr3stgrlem4  48734  isubgr3stgrlem6  48736  isubgr3stgrlem7  48737  uspgrlimlem3  48755  grlimedgclnbgr  48760  grlimgrtrilem2  48767  grlimgrtri  48768  grlicsym  48778  gpgedgvtx1  48827  gpgedgiov  48830  gpgedg2ov  48831  gpgedg2iv  48832  pgnioedg1  48873  pgnioedg2  48874  pgnioedg3  48875  pgnioedg4  48876  pgnioedg5  48877  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  pgnbgreunbgrlem5lem1  48885  pgnbgreunbgrlem5lem2  48886  pgnbgreunbgrlem5lem3  48887  lcosslsp  49218  lindslinindsimp1  49237  snlindsntor  49251  itcovalt2  49457  eenglngeehlnmlem2  49518  itsclc0yqsol  49544  itschlc0xyqsol1  49546  itschlc0xyqsol  49547  opnneilv  49687  i0oii  49698  io1ii  49699  iscnrm3lem4  49714  iscnrm3r  49726  setrec1lem4  50468  aacllem  50621