Theorem syld 48

Description: Syllogism deduction. Deduction associated with syl 18. See conventions 30798 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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldc  49  3syld  61  sylsyld  62  nsyld  157  pm2.61d  181  sylibd  242  sylbid  243  sylibrd  262  sylbird  263  syland  615  animpimp2impd  860  ax12v2  2218  alrimdd  2253  axc16g  2298  axc16nf  2301  axc11r  2402  sb4a  2514  2eu1  2680  2eu1v  2681  ss2ralv  4009  ss2rexv  4010  trel3  5229  poss  5573  sess2  5629  wefrc  5657  wereu2  5660  predtrss  6327  frpomin  6345  ordpss  6393  funun  6586  ssimaex  6970  f1cofveqaeq  7257  f1imass  7264  soisoi  7332  isores3  7339  isofrlem  7344  isoselem  7345  weniso  7360  abnexg  7757  oninton  7796  orduniorsuc  7828  limuni3  7850  tfindsg  7859  limom  7880  resf1extb  7933  f1o2ndf1  8119  soxp  8127  xpord3inddlem  8152  soseq  8157  extmptsuppeq  8186  smoel  8349  tfrlem9  8374  tz7.49  8434  seqomlem1  8439  odi  8566  omass  8567  omeulem2  8570  oeordsuc  8582  oeeulem  8589  naddsuc2  8690  ertr  8712  swoord2  8730  ecopovtrn  8820  domtriord  9114  pssnn  9156  unxpdomlem2  9220  isinf  9228  f1finf1o  9236  findcard3  9246  frfi  9248  unblem3  9257  supssd  9426  infssd  9457  en3lplem1  9584  inf3lem5  9604  cantnfle  9643  cantnfp1lem3  9652  ttrcltr  9688  frmin  9724  rankxpsuc  9857  tcrank  9859  ficardom  9959  carduni  9979  infxpenlem  10009  dfac8alem  10025  ac10ct  10030  ween  10031  alephdom  10077  alephle  10084  iscard3  10089  alephfp  10104  pwsdompw  10198  infdif  10203  cfslbn  10262  cofsmo  10264  cfcof  10269  fin1a2s  10409  domtriomlem  10437  ac6num  10474  zorn2lem3  10493  axdclem2  10515  imadomg  10529  iundom2g  10535  ficard  10560  fpwwe2lem7  10633  fpwwe2  10639  gchpwdom  10666  gchaclem  10674  tskr1om2  10764  inar1  10771  tskord  10776  tskuni  10779  grudomon  10813  grur1a  10815  grur1  10816  addnidpi  10897  ltexnq  10971  genpnnp  11001  addclprlem2  11013  mulclprlem  11015  psslinpr  11027  ltexprlem6  11037  ltexprlem7  11038  addcanpr  11042  mulgt0sr  11101  map2psrpr  11106  supsrlem  11107  axrrecex  11159  letr  11315  dedekind  11384  recex  11857  lemul12b  12083  fimaxre2  12171  lbreu  12176  nnrecgt0  12290  nnunb  12511  bndndx  12514  zeo  12694  uzind  12700  fzind  12706  fnn0ind  12707  suprfinzcl  12722  suprzcl2  12974  zmax  12981  rpnnen1lem5  13017  xrletr  13195  qbtwnre  13237  qsqueeze  13239  qextltlem  13240  xralrple  13243  xlesubadd  13301  supxrunb1  13357  icoshft  13512  zltaddlt1le  13544  fzen  13581  elfz0fzfz0  13674  elfzmlbp  13680  elfzo0z  13743  fzofzim  13751  fzo1fzo0n0  13757  elfzodifsumelfzo  13773  ssfzoulel  13802  modadd1  13955  modmul1  13974  uzrdgfni  14008  fsuppmapnn0fiub0  14043  fsuppmapnn0ub  14045  fsuppmapnn0fz  14046  seqf1olem1  14091  seqf1olem2  14092  expnbnd  14282  faclbnd4lem4  14346  hashgt23el  14475  seqcoll  14515  hashle2pr  14528  elss2prb  14539  ccatalpha  14646  swrdsbslen  14720  swrdspsleq  14721  swrdswrdlem  14759  swrdswrd  14760  pfxccatin12lem2a  14782  pfxccatin12lem1  14783  pfxccatin12lem3  14787  swrdccat3blem  14794  reuccatpfxs1lem  14801  repswswrd  14841  cshf1  14867  swrd2lsw  15009  sqeqd  15237  sqrmo  15322  cau3lem  15426  icodiamlt  15509  limsupbnd2  15554  lo1bdd2  15595  climuni  15623  rlimcn3  15661  mulcn2  15667  o1of2  15684  rlimo1  15688  lo1le  15723  iseralt  15756  cvgrat  15956  fprodss  16021  rpnnen2lem12  16299  ruclem3  16307  sqrt2irr  16323  p1modz1  16335  dvdsmodexp  16336  dvds2lem  16344  dvdslelem  16385  dvdsabseq  16389  divalglem8  16476  bitsinv1lem  16517  sadcaddlem  16533  smu01lem  16561  smueqlem  16566  bezoutlem4  16618  dfgcd2  16622  algcvga  16655  lcmfunsnlem1  16713  lcmfunsnlem2lem1  16714  lcmfunsnlem2lem2  16715  lcmfdvdsb  16719  coprmgcdb  16725  coprmdvds2  16730  coprmprod  16737  isprm3  16759  prmdvdsfz  16782  isprm5  16784  coprm  16788  rpexp12i  16801  phibndlem  16847  dfphi2  16851  eulerthlem2  16859  odzdvds  16873  iserodd  16913  pclem  16916  pcpremul  16921  pcqcl  16934  pcdvdsb  16947  pcprmpw2  16960  difsqpwdvds  16965  pcaddlem  16966  pcmptcl  16969  pcfac  16977  prmpwdvds  16982  unbenlem  16986  prmreclem1  16994  4sqlem17  17039  vdwmc2  17057  vdwlem9  17067  vdwlem10  17068  vdwlem13  17071  vdwnnlem3  17075  ramcl  17107  prmgaplem7  17135  mreiincl  17666  initoid  18076  termoid  18077  initoeu2lem1  18089  pospo  18417  resspos  18503  resstos  18504  dirge  18677  cyccom  19298  gsmsymgrfixlem1  19521  oddvdsnn0  19638  oddvds  19641  odcl2  19659  gexdvds  19678  sylow2alem2  19712  sylow2a  19713  efgi2  19819  efgsrel  19828  efgs1b  19830  imasabl  19970  cyggex2  19991  telgsums  20087  pgpfac1lem2  20171  pgpfac1lem3a  20172  pgpfac1lem3  20173  pgpfac1lem5  20175  crngrhmfo  20604  zrtermorngc  20772  zrtermoringc  20804  lmodfopnelem2  21050  lssssr  21105  rnglidlmcl  21371  unichnlidl  21392  gzrngunitlem  21612  znunit  21743  frgpcyg  21753  lsmcss  21872  obselocv  21908  obslbs  21910  mhpvarcl  22341  cply1mul  22486  gsummoncoe1  22498  cpmatacl  22903  cpmatinvcl  22904  cpmatmcllem  22905  m2cpminvid2lem  22941  mp2pm2mplem4  22996  pm2mp  23012  chfacfisf  23041  chfacfisfcpmat  23042  chfacfscmul0  23045  chfacfpmmul0  23049  cayhamlem4  23075  ordtrest2lem  23390  leordtval2  23399  lecldbas  23406  cncls  23461  cncnp  23467  cnpresti  23475  lmcnp  23491  cnt0  23533  isreg2  23564  cmpsublem  23586  cmpsub  23587  tgcmp  23588  bwth  23597  dfconn2  23606  1stcfb  23632  1stcelcls  23649  islly2  23672  dislly  23685  reftr  23702  comppfsc  23720  kgencn2  23745  txcnp  23808  txindis  23822  txcmplem1  23829  txlm  23836  xkohaus  23841  cnmptcom  23866  kqfvima  23918  isr0  23925  fgss2  24062  fbasrn  24072  filuni  24073  ufilmax  24095  isufil2  24096  cfinufil  24116  fmfnfmlem1  24142  fmfnfmlem2  24143  fmfnfmlem4  24145  fmfnfm  24146  fmco  24149  flimopn  24163  hausflim  24169  flimrest  24171  fclsopn  24202  flimfnfcls  24216  alexsubALTlem2  24236  alexsubALTlem3  24237  alexsubALT  24239  ptcmplem2  24241  cnextcn  24255  symgtgp  24294  qustgplem  24309  tsmsres  24332  tsmsxplem1  24341  isucn2  24466  imasdsf1olem  24561  bldisj  24586  blssps  24612  blss  24613  metcnp3  24728  ngptgp  24824  nrginvrcn  24880  nmoleub  24919  xrsmopn  25001  icccmplem3  25013  reconnlem2  25016  rectbntr0  25021  rescncf  25087  iocopnst  25130  iccpnfcnv  25134  lebnumii  25156  nmoleub2lem  25304  nmhmcn  25310  iscfil3  25463  iscau2  25467  iscau3  25468  iscau4  25469  iscmet3lem2  25482  caussi  25487  equivcfil  25489  equivcau  25490  ivthlem2  25642  ivthlem3  25643  ovoliunlem2  25693  ovoliunnul  25697  ioombl1lem4  25751  dyadmax  25788  dyadmbl  25790  volsup2  25795  itg2le  25929  itg2const2  25931  itg2seq  25932  itgsplitioo  26028  rolle  26180  c1lip1  26187  dvivthlem1  26198  lhop1  26204  dvcnvrelem1  26207  dvfsumrlim  26221  ply1divmo  26324  ig1peu  26363  plypf1  26400  coeaddlem  26437  dvply2g  26477  fta1  26500  quotcan  26501  aalioulem4  26529  ulmcaulem  26588  ulmcn  26593  pilem2  26646  sincosq1lem  26693  sinq12gt0  26703  sinq12ge0  26704  tanord1  26733  lognegb  26786  logrec  26959  logbgcd1irr  26990  dcubic  27042  xrlimcnp  27164  o1cxp  27170  ftalem2  27269  ftalem3  27270  fsumdvdscom  27380  chtub  27407  vmasum  27411  bcmono  27472  bposlem3  27481  bposlem7  27485  lgsdir  27527  lgsqrlem2  27542  lgsqrmodndvds  27548  gausslemma2dlem6  27567  gausslemma2d  27569  lgsquadlem2  27576  2lgslem3a1  27595  2lgslem3b1  27596  2lgslem3c1  27597  2lgslem3d1  27598  2sqlem6  27618  2sq2  27628  2sqmod  27631  dchrisumlem3  27686  pntrsumbnd2  27762  pntpbnd1  27781  pntibnd  27788  pntlem3  27804  pntleml  27806  ltsres  27857  nosepon  27860  nolesgn2o  27866  nogesgn1o  27868  nodenselem8  27886  nosupbnd1lem1  27903  madess  28090  madebdaylemlrcut  28123  peano5uzs  28628  bdayfinbndlem1  28691  z12bday  28709  brbtwn2  29286  colinearalg  29291  axcontlem10  29354  edgupgr  29515  edglnl  29524  usgruspgrb  29567  subupgr  29671  uhgrspan1  29687  usgredgsscusgredg  29843  fusgrn0degnn0  29883  upgrewlkle2  29990  uspgr2wlkeq  30029  redwlk  30054  wlkdlem2  30065  upgrwlkdvdelem  30125  pthdlem1  30155  pthdlem2  30157  crctcshwlkn0lem3  30204  wlkiswwlks1  30259  wwlksm1edg  30273  wwlksnred  30284  wwlksnextbi  30286  umgr2adedgspth  30340  clwlkclwwlklem2fv2  30390  clwlkclwwlklem2a  30392  clwlkclwwlkf1lem3  30400  clwwisshclwwslemlem  30407  clwwlkf  30441  clwwlkext2edg  30450  wwlksubclwwlk  30452  clwwlknonex2lem2  30502  loop1cycl  30547  eupth2lems  30636  frgrwopreglem4a  30708  frgrregorufrg  30724  ex-natded5.3-2  30806  isgrpo  30896  vacn  31093  ubthlem2  31270  htthlem  31316  normgt0  31526  shmodsi  31788  spansneleq  31969  h1datomi  31980  nmcexi  32425  pjnormssi  32567  stm1add3i  32646  golem2  32671  cvnsym  32689  dmdmd  32699  mdslmd1lem1  32724  mdslmd1i  32728  mdexchi  32734  atcveq0  32747  superpos  32753  hatomistici  32761  atoml2i  32782  atcvat2i  32786  chirredlem1  32789  atcvat3i  32795  mdsymlem3  32804  mdsymlem5  32806  cdj3lem2b  32836  cdj3i  32840  submarchi  33546  dfufd2  33880  tpr2rico  34342  ordtrest2NEWlem  34352  xrge0iifcnv  34363  omssubadd  34731  eulerpartlemb  34799  ballotlemfc0  34924  ballotlemfcc  34925  ftc2re  35026  fissorduni  35514  fineqvinfep  35571  axsepg2  35586  axsepg4  35589  axpowg2  35593  axpowg3  35594  subfacp1lem6  35690  iccllysconn  35755  cvmfolem  35784  satfsschain  35869  satfrel  35872  satfdm  35874  sat1el2xp  35884  satffunlem1lem1  35907  dmopab3rexdif  35910  satffunlem2lem2  35911  satffun  35914  fundmpss  36272  dfon2lem3  36288  dfon2lem6  36291  axextbdist  36303  dfrdg4  36456  5segofs  36511  cgrextend  36513  segconeu  36516  btwncomim  36518  btwnswapid  36522  btwnintr  36524  btwnexch3  36525  btwndiff  36532  ifscgr  36549  cgrxfr  36560  btwnxfr  36561  lineext  36581  brofs2  36582  linecgr  36586  lineid  36588  idinside  36589  endofsegid  36590  btwnconn1lem13  36604  btwnconn3  36608  finminlem  36862  nn0prpwlem  36866  cldbnd  36870  clsint2  36873  fnessref  36901  neibastop3  36906  fgmin  36914  onsuct0  36985  limsucncmpi  36989  tr0elw  37028  tr0el  37029  bj-nnfea  37392  bj-axc14  37524  bj-restn0  37765  bj-0int  37776  wl-19.2reqv  38212  wl-aetr  38217  wl-axc11r  38218  fin2so  38291  tan2h  38296  lindsenlbs  38299  poimirlem2  38306  poimirlem9  38313  poimirlem17  38321  poimirlem18  38322  poimirlem21  38325  poimirlem23  38327  poimirlem26  38330  poimirlem29  38333  poimirlem30  38334  poimirlem31  38335  poimir  38337  heicant  38339  mblfinlem2  38342  mblfinlem3  38343  itg2addnclem  38355  itg2addnclem2  38356  itg2gt0cn  38359  ftc1anclem5  38381  ftc1anclem6  38382  filbcmb  38424  nninfnub  38435  mettrifi  38441  geomcau  38443  istotbnd3  38455  sstotbnd2  38458  ismtybndlem  38490  heibor1lem  38493  heiborlem1  38495  heiborlem8  38502  heiborlem10  38504  heibor  38505  opidonOLD  38536  riscer  38672  crngohomfo  38690  keridl  38716  ispridl2  38722  ispridlc  38754  ac6s6  38854  eqvreltr  39373  eldisjdmqsim  39499  suceldisj  39500  eldisjs6  39622  dral1-o  39711  ax12indalem  39752  ax12inda2ALT  39753  lsatcveq0  39839  eqlkr3  39908  atlatmstc  40126  atlrelat1  40128  hlrelat2  40210  intnatN  40214  cvrexchlem  40226  cvratlem  40228  cvrat2  40236  atltcvr  40242  cvrat3  40249  cvrat4  40250  ps-1  40284  ps-2  40285  lplnnle2at  40348  lvolnle3at  40389  2llnma3r  40595  cdlemblem  40600  pmapjoin  40659  elpcliN  40700  lhpmcvr4N  40833  4atexlemnclw  40877  trlnidatb  40984  cdlemc4  41001  cdlemd3  41007  cdleme3g  41041  cdleme7d  41053  cdleme11c  41068  cdleme11dN  41069  cdleme21b  41133  cdleme21c  41134  cdleme21i  41142  cdleme22b  41148  cdleme35fnpq  41256  cdlemf1  41368  trlord  41376  cdlemg6c  41427  dihglblem6  42147  dochlkr  42192  dochkrshp  42193  dihjat1lem  42235  dochexmidlem5  42271  dochexmidlem8  42274  qsalrel  43042  remulcand  43233  prjspner1  43391  fphpdo  43577  pellexlem5  43593  pellexlem6  43594  jm2.26lem3  43761  unxpwdom3  43855  omlimcl2  44002  oe0suclim  44037  cantnfresb  44084  tfsconcatb0  44104  naddgeoa  44154  iscard5  44295  sqrtcval  44400  ov2ssiunov2  44459  frege124d  44520  19.41rg  45292  relpfrlem  45695  modelaxreplem2  45721  stoweidlem34  46781  ormklocald  47623  evenwodadd  47635  cfsetsnfsetf1  47829  fcoresf1  47839  euoreqb  47879  2reu8i  47883  ralralimp  48048  f1oresf1o2  48061  zm1nn  48072  elfz2z  48085  2tceilhalfelfzo1  48106  m1modmmod  48134  modlt0b  48139  muldvdsfacgt  48156  muldvdsfacm1  48157  iccpartlt  48206  iccelpart  48215  icceuelpartlem  48217  fargshiftf1  48223  sprsymrelf1lem  48273  paireqne  48293  reuopreuprim  48308  goldbachthlem2  48331  odz2prm2pw  48348  fmtnoprmfac1lem  48349  fmtnofac2lem  48353  prmdvdsfmtnof1  48372  sfprmdvdsmersenne  48388  lighneallem2  48391  lighneallem4  48395  fppr2odd  48529  gbegt5  48559  gbowge7  48561  bgoldbtbndlem4  48606  bgoldbtbnd  48607  tgoldbach  48615  grimuhgr  48685  grimcnv  48686  grimco  48687  isuspgrim0  48692  isuspgrimlem  48693  upgrimwlklem5  48699  upgrimtrlslem2  48703  uhgrimisgrgriclem  48728  clnbgrgrimlem  48731  clnbgrgrim  48732  grimedg  48733  grtriprop  48739  isubgr3stgrlem3  48766  isubgr3stgrlem4  48767  isubgr3stgrlem6  48769  isubgr3stgrlem7  48770  uspgrlimlem3  48788  grlimedgclnbgr  48793  grlimgrtrilem2  48800  grlimgrtri  48801  grlicsym  48811  gpgedgvtx1  48860  gpgedgiov  48863  gpgedg2ov  48864  gpgedg2iv  48865  pgnioedg1  48906  pgnioedg2  48907  pgnioedg3  48908  pgnioedg4  48909  pgnioedg5  48910  pgnbgreunbgrlem2lem1  48912  pgnbgreunbgrlem2lem2  48913  pgnbgreunbgrlem2lem3  48914  pgnbgreunbgrlem5lem1  48918  pgnbgreunbgrlem5lem2  48919  pgnbgreunbgrlem5lem3  48920  lcosslsp  49251  lindslinindsimp1  49270  snlindsntor  49284  itcovalt2  49490  eenglngeehlnmlem2  49551  itsclc0yqsol  49577  itschlc0xyqsol1  49579  itschlc0xyqsol  49580  opnneilv  49720  i0oii  49731  io1ii  49732  iscnrm3lem4  49747  iscnrm3r  49759  setrec1lem4  50501  aacllem  50654