Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30559 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 25	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpdd 43	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  48  3syld  60  sylsyld  61  nsyld  156  pm2.61d  180  sylibd  241  sylbid  242  sylibrd  261  sylbird  262  syland  612  animpimp2impd  857  ax12v2  2213  alrimdd  2248  axc16g  2294  axc16nf  2297  axc11r  2398  sb4a  2510  2eu1  2676  2eu1v  2677  ss2ralv  4005  ss2rexv  4006  trel3  5213  poss  5553  sess2  5609  wefrc  5637  wereu2  5640  predtrss  6304  frpomin  6322  funun  6562  ssimaex  6947  f1cofveqaeq  7236  f1imass  7243  soisoi  7307  isores3  7314  isofrlem  7319  isoselem  7320  weniso  7333  abnexg  7734  oninton  7773  orduniorsuc  7805  limuni3  7827  tfindsg  7836  limom  7857  resf1extb  7910  f1o2ndf1  8095  soxp  8103  xpord3inddlem  8128  soseq  8133  extmptsuppeq  8162  smoel  8325  tfrlem9  8350  tz7.49  8410  seqomlem1  8415  odi  8542  omass  8543  omeulem2  8546  oeordsuc  8558  oeeulem  8565  naddsuc2  8666  ertr  8688  swoord2  8706  ecopovtrn  8796  domtriord  9089  pssnn  9131  unxpdomlem2  9195  isinf  9203  f1finf1o  9211  findcard3  9221  frfi  9223  unblem3  9232  supssd  9403  infssd  9434  en3lplem1  9561  inf3lem5  9581  cantnfle  9620  cantnfp1lem3  9629  ttrcltr  9665  frmin  9701  rankxpsuc  9834  tcrank  9836  ficardom  9913  carduni  9933  infxpenlem  9963  dfac8alem  9979  ac10ct  9984  ween  9985  alephdom  10031  alephle  10038  iscard3  10043  alephfp  10058  pwsdompw  10153  infdif  10158  cfslbn  10218  cofsmo  10220  cfcof  10225  fin1a2s  10365  domtriomlem  10393  ac6num  10430  zorn2lem3  10449  axdclem2  10471  imadomg  10485  iundom2g  10491  ficard  10516  fpwwe2lem7  10589  fpwwe2  10595  gchpwdom  10622  gchaclem  10630  tskr1om2  10720  inar1  10727  tskord  10732  tskuni  10735  grudomon  10769  grur1a  10771  grur1  10772  addnidpi  10853  ltexnq  10927  genpnnp  10957  addclprlem2  10969  mulclprlem  10971  psslinpr  10983  ltexprlem6  10993  ltexprlem7  10994  addcanpr  10998  mulgt0sr  11057  map2psrpr  11062  supsrlem  11063  axrrecex  11115  letr  11271  dedekind  11340  recex  11813  lemul12b  12042  mulgt1OLD  12044  fimaxre2  12131  lbreu  12136  nnrecgt0  12250  nnunb  12471  bndndx  12474  zeo  12653  uzind  12659  fzind  12665  fnn0ind  12666  suprfinzcl  12681  suprzcl2  12933  zmax  12940  rpnnen1lem5  12976  xrletr  13154  qbtwnre  13196  qsqueeze  13198  qextltlem  13199  xralrple  13202  xlesubadd  13260  supxrunb1  13316  icoshft  13471  zltaddlt1le  13503  fzen  13540  elfz0fzfz0  13632  elfzmlbp  13638  elfzo0z  13701  fzofzim  13709  fzo1fzo0n0  13715  elfzodifsumelfzo  13731  ssfzoulel  13760  modadd1  13912  modmul1  13931  uzrdgfni  13965  fsuppmapnn0fiub0  14000  fsuppmapnn0ub  14002  fsuppmapnn0fz  14003  seqf1olem1  14048  seqf1olem2  14049  expnbnd  14239  faclbnd4lem4  14303  hashgt23el  14431  seqcoll  14471  hashle2pr  14484  elss2prb  14495  ccatalpha  14601  swrdsbslen  14672  swrdspsleq  14673  swrdswrdlem  14711  swrdswrd  14712  pfxccatin12lem2a  14734  pfxccatin12lem1  14735  pfxccatin12lem3  14739  swrdccat3blem  14746  reuccatpfxs1lem  14753  repswswrd  14791  cshf1  14817  swrd2lsw  14959  sqeqd  15184  sqrmo  15269  cau3lem  15373  icodiamlt  15456  limsupbnd2  15501  lo1bdd2  15542  climuni  15570  rlimcn3  15608  mulcn2  15614  o1of2  15631  rlimo1  15635  lo1le  15670  iseralt  15703  cvgrat  15904  fprodss  15969  rpnnen2lem12  16248  ruclem3  16256  sqrt2irr  16272  p1modz1  16284  dvdsmodexp  16285  dvds2lem  16293  dvdslelem  16334  dvdsabseq  16338  divalglem8  16425  bitsinv1lem  16466  sadcaddlem  16482  smu01lem  16510  smueqlem  16515  bezoutlem4  16567  dfgcd2  16571  algcvga  16604  lcmfunsnlem1  16662  lcmfunsnlem2lem1  16663  lcmfunsnlem2lem2  16664  lcmfdvdsb  16668  coprmgcdb  16674  coprmdvds2  16679  coprmprod  16686  isprm3  16708  prmdvdsfz  16731  isprm5  16733  coprm  16737  rpexp12i  16750  phibndlem  16796  dfphi2  16800  eulerthlem2  16808  odzdvds  16822  iserodd  16862  pclem  16865  pcpremul  16870  pcqcl  16883  pcdvdsb  16896  pcprmpw2  16909  difsqpwdvds  16914  pcaddlem  16915  pcmptcl  16918  pcfac  16926  prmpwdvds  16931  unbenlem  16935  prmreclem1  16943  4sqlem17  16988  vdwmc2  17006  vdwlem9  17016  vdwlem10  17017  vdwlem13  17020  vdwnnlem3  17024  ramcl  17056  prmgaplem7  17084  mreiincl  17615  initoid  18025  termoid  18026  initoeu2lem1  18038  pospo  18366  resspos  18452  resstos  18453  dirge  18626  cyccom  19235  gsmsymgrfixlem1  19458  oddvdsnn0  19575  oddvds  19578  odcl2  19596  gexdvds  19615  sylow2alem2  19649  sylow2a  19650  efgi2  19756  efgsrel  19765  efgs1b  19767  imasabl  19907  cyggex2  19928  telgsums  20024  pgpfac1lem2  20108  pgpfac1lem3a  20109  pgpfac1lem3  20110  pgpfac1lem5  20112  zrtermorngc  20680  zrtermoringc  20712  lmodfopnelem2  20954  lssssr  21009  rnglidlmcl  21274  gzrngunitlem  21472  znunit  21603  frgpcyg  21613  lsmcss  21732  obselocv  21768  obslbs  21770  mhpvarcl  22201  cply1mul  22347  gsummoncoe1  22359  cpmatacl  22764  cpmatinvcl  22765  cpmatmcllem  22766  m2cpminvid2lem  22802  mp2pm2mplem4  22857  pm2mp  22873  chfacfisf  22902  chfacfisfcpmat  22903  chfacfscmul0  22906  chfacfpmmul0  22910  cayhamlem4  22936  ordtrest2lem  23251  leordtval2  23260  lecldbas  23267  cncls  23322  cncnp  23328  cnpresti  23336  lmcnp  23352  cnt0  23394  isreg2  23425  cmpsublem  23447  cmpsub  23448  tgcmp  23449  bwth  23458  dfconn2  23467  1stcfb  23493  1stcelcls  23509  islly2  23532  dislly  23545  reftr  23562  comppfsc  23580  kgencn2  23605  txcnp  23668  txindis  23682  txcmplem1  23689  txlm  23696  xkohaus  23701  cnmptcom  23726  kqfvima  23778  isr0  23785  fgss2  23922  fbasrn  23932  filuni  23933  ufilmax  23955  isufil2  23956  cfinufil  23976  fmfnfmlem1  24002  fmfnfmlem2  24003  fmfnfmlem4  24005  fmfnfm  24006  fmco  24009  flimopn  24023  hausflim  24029  flimrest  24031  fclsopn  24062  flimfnfcls  24076  alexsubALTlem2  24096  alexsubALTlem3  24097  alexsubALT  24099  ptcmplem2  24101  cnextcn  24115  symgtgp  24154  qustgplem  24169  tsmsres  24192  tsmsxplem1  24201  isucn2  24326  imasdsf1olem  24421  bldisj  24446  blssps  24472  blss  24473  metcnp3  24588  ngptgp  24684  nrginvrcn  24740  nmoleub  24779  xrsmopn  24861  icccmplem3  24873  reconnlem2  24876  rectbntr0  24881  rescncf  24947  iocopnst  24990  iccpnfcnv  24994  lebnumii  25016  nmoleub2lem  25164  nmhmcn  25170  iscfil3  25323  iscau2  25327  iscau3  25328  iscau4  25329  iscmet3lem2  25342  caussi  25347  equivcfil  25349  equivcau  25350  ivthlem2  25502  ivthlem3  25503  ovoliunlem2  25553  ovoliunnul  25557  ioombl1lem4  25611  dyadmax  25648  dyadmbl  25650  volsup2  25655  itg2le  25789  itg2const2  25791  itg2seq  25792  itgsplitioo  25888  rolle  26040  c1lip1  26047  dvivthlem1  26058  lhop1  26064  dvcnvrelem1  26067  dvfsumrlim  26081  ply1divmo  26184  ig1peu  26223  plypf1  26260  coeaddlem  26297  dvply2g  26337  fta1  26360  quotcan  26361  aalioulem4  26387  ulmcaulem  26445  ulmcn  26450  pilem2  26503  sincosq1lem  26550  sinq12gt0  26560  sinq12ge0  26561  tanord1  26590  lognegb  26643  logrec  26816  logbgcd1irr  26847  dcubic  26899  xrlimcnp  27021  o1cxp  27027  ftalem2  27126  ftalem3  27127  fsumdvdscom  27237  chtub  27264  vmasum  27268  bcmono  27329  bposlem3  27338  bposlem7  27342  lgsdir  27384  lgsqrlem2  27399  lgsqrmodndvds  27405  gausslemma2dlem6  27424  gausslemma2d  27426  lgsquadlem2  27433  2lgslem3a1  27452  2lgslem3b1  27453  2lgslem3c1  27454  2lgslem3d1  27455  2sqlem6  27475  2sq2  27485  2sqmod  27488  dchrisumlem3  27543  pntrsumbnd2  27619  pntpbnd1  27638  pntibnd  27645  pntlem3  27661  pntleml  27663  ltsres  27714  nosepon  27717  nolesgn2o  27723  nogesgn1o  27725  nodenselem8  27743  nosupbnd1lem1  27760  madess  27947  madebdaylemlrcut  27980  peano5uzs  28485  bdayfinbndlem1  28548  z12bday  28566  brbtwn2  29063  colinearalg  29068  axcontlem10  29131  edgupgr  29292  edglnl  29301  usgruspgrb  29341  subupgr  29445  uhgrspan1  29461  usgredgsscusgredg  29617  fusgrn0degnn0  29657  upgrewlkle2  29764  uspgr2wlkeq  29803  redwlk  29828  wlkdlem2  29839  upgrwlkdvdelem  29893  pthdlem1  29923  pthdlem2  29925  crctcshwlkn0lem3  29969  wlkiswwlks1  30024  wwlksm1edg  30038  wwlksnred  30049  wwlksnextbi  30051  umgr2adedgspth  30105  clwlkclwwlklem2fv2  30155  clwlkclwwlklem2a  30157  clwlkclwwlkf1lem3  30165  clwwisshclwwslemlem  30172  clwwlkf  30206  clwwlkext2edg  30215  wwlksubclwwlk  30217  clwwlknonex2lem2  30267  eupth2lems  30397  frgrwopreglem4a  30469  frgrregorufrg  30485  ex-natded5.3-2  30567  isgrpo  30657  vacn  30854  ubthlem2  31031  htthlem  31077  normgt0  31287  shmodsi  31549  spansneleq  31730  h1datomi  31741  nmcexi  32186  pjnormssi  32328  stm1add3i  32407  golem2  32432  cvnsym  32450  dmdmd  32460  mdslmd1lem1  32485  mdslmd1i  32489  mdexchi  32495  atcveq0  32508  superpos  32514  hatomistici  32522  atoml2i  32543  atcvat2i  32547  chirredlem1  32550  atcvat3i  32556  mdsymlem3  32565  mdsymlem5  32567  cdj3lem2b  32597  cdj3i  32601  submarchi  33327  dfufd2  33707  tpr2rico  34170  ordtrest2NEWlem  34180  xrge0iifcnv  34191  omssubadd  34558  eulerpartlemb  34626  ballotlemfc0  34751  ballotlemfcc  34752  ftc2re  34853  fissorduni  35346  fineqvinfep  35382  axsepg2  35397  axsepg4  35400  axpowg2  35404  axpowg3  35405  loop1cycl  35448  subfacp1lem6  35496  iccllysconn  35561  cvmfolem  35590  satfsschain  35675  satfrel  35678  satfdm  35680  sat1el2xp  35690  satffunlem1lem1  35713  dmopab3rexdif  35716  satffunlem2lem2  35717  satffun  35720  fundmpss  36078  dfon2lem3  36094  dfon2lem6  36097  axextbdist  36109  dfrdg4  36262  5segofs  36317  cgrextend  36319  segconeu  36322  btwncomim  36324  btwnswapid  36328  btwnintr  36330  btwnexch3  36331  btwndiff  36338  ifscgr  36355  cgrxfr  36366  btwnxfr  36367  lineext  36387  brofs2  36388  linecgr  36392  lineid  36394  idinside  36395  endofsegid  36396  btwnconn1lem13  36410  btwnconn3  36414  finminlem  36639  nn0prpwlem  36643  cldbnd  36647  clsint2  36650  fnessref  36678  neibastop3  36683  fgmin  36691  onsuct0  36762  limsucncmpi  36766  tr0elw  36805  tr0el  36806  bj-nnfea  37170  bj-axc14  37302  bj-restn0  37541  bj-0int  37552  wl-19.2reqv  37988  wl-aetr  37993  wl-axc11r  37994  fin2so  38067  tan2h  38072  lindsenlbs  38075  poimirlem2  38082  poimirlem9  38089  poimirlem17  38097  poimirlem18  38098  poimirlem21  38101  poimirlem23  38103  poimirlem26  38106  poimirlem29  38109  poimirlem30  38110  poimirlem31  38111  poimir  38113  heicant  38115  mblfinlem2  38118  mblfinlem3  38119  itg2addnclem  38131  itg2addnclem2  38132  itg2gt0cn  38135  ftc1anclem5  38157  ftc1anclem6  38158  filbcmb  38200  nninfnub  38211  mettrifi  38217  geomcau  38219  istotbnd3  38231  sstotbnd2  38234  ismtybndlem  38266  heibor1lem  38269  heiborlem1  38271  heiborlem8  38278  heiborlem10  38280  heibor  38281  opidonOLD  38312  riscer  38448  crngohomfo  38466  keridl  38492  ispridl2  38498  ispridlc  38530  ac6s6  38632  eqvreltr  39151  eldisjdmqsim  39277  suceldisj  39278  eldisjs6  39400  dral1-o  39489  ax12indalem  39530  ax12inda2ALT  39531  lsatcveq0  39617  eqlkr3  39686  atlatmstc  39904  atlrelat1  39906  hlrelat2  39988  intnatN  39992  cvrexchlem  40004  cvratlem  40006  cvrat2  40014  atltcvr  40020  cvrat3  40027  cvrat4  40028  ps-1  40062  ps-2  40063  lplnnle2at  40126  lvolnle3at  40167  2llnma3r  40373  cdlemblem  40378  pmapjoin  40437  elpcliN  40478  lhpmcvr4N  40611  4atexlemnclw  40655  trlnidatb  40762  cdlemc4  40779  cdlemd3  40785  cdleme3g  40819  cdleme7d  40831  cdleme11c  40846  cdleme11dN  40847  cdleme21b  40911  cdleme21c  40912  cdleme21i  40920  cdleme22b  40926  cdleme35fnpq  41034  cdlemf1  41146  trlord  41154  cdlemg6c  41205  dihglblem6  41925  dochlkr  41970  dochkrshp  41971  dihjat1lem  42013  dochexmidlem5  42049  dochexmidlem8  42052  qsalrel  42818  remulcand  43009  prjspner1  43169  fphpdo  43355  pellexlem5  43371  pellexlem6  43372  jm2.26lem3  43539  unxpwdom3  43633  omlimcl2  43780  oe0suclim  43815  cantnfresb  43862  tfsconcatb0  43882  naddgeoa  43932  iscard5  44073  sqrtcval  44178  ov2ssiunov2  44237  frege124d  44298  ordpss  44987  19.41rg  45087  relpfrlem  45490  modelaxreplem2  45516  stoweidlem34  46569  ormklocald  47411  evenwodadd  47424  cfsetsnfsetf1  47614  fcoresf1  47624  euoreqb  47664  2reu8i  47668  ralralimp  47833  f1oresf1o2  47846  zm1nn  47857  elfz2z  47870  2tceilhalfelfzo1  47891  m1modmmod  47919  modlt0b  47924  muldvdsfacgt  47941  muldvdsfacm1  47942  iccpartlt  47991  iccelpart  48000  icceuelpartlem  48002  fargshiftf1  48008  sprsymrelf1lem  48058  paireqne  48078  reuopreuprim  48093  goldbachthlem2  48116  odz2prm2pw  48133  fmtnoprmfac1lem  48134  fmtnofac2lem  48138  prmdvdsfmtnof1  48157  sfprmdvdsmersenne  48173  lighneallem2  48176  lighneallem4  48180  fppr2odd  48314  gbegt5  48344  gbowge7  48346  bgoldbtbndlem4  48391  bgoldbtbnd  48392  tgoldbach  48400  grimuhgr  48470  grimcnv  48471  grimco  48472  isuspgrim0  48477  isuspgrimlem  48478  upgrimwlklem5  48484  upgrimtrlslem2  48488  uhgrimisgrgriclem  48513  clnbgrgrimlem  48516  clnbgrgrim  48517  grimedg  48518  grtriprop  48524  isubgr3stgrlem3  48551  isubgr3stgrlem4  48552  isubgr3stgrlem6  48554  isubgr3stgrlem7  48555  uspgrlimlem3  48573  grlimedgclnbgr  48578  grlimgrtrilem2  48585  grlimgrtri  48586  grlicsym  48596  gpgedgvtx1  48645  gpgedgiov  48648  gpgedg2ov  48649  gpgedg2iv  48650  pgnioedg1  48691  pgnioedg2  48692  pgnioedg3  48693  pgnioedg4  48694  pgnioedg5  48695  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  pgnbgreunbgrlem5lem1  48703  pgnbgreunbgrlem5lem2  48704  pgnbgreunbgrlem5lem3  48705  lcosslsp  49021  lindslinindsimp1  49040  snlindsntor  49054  itcovalt2  49260  eenglngeehlnmlem2  49321  itsclc0yqsol  49347  itschlc0xyqsol1  49349  itschlc0xyqsol  49350  opnneilv  49491  i0oii  49502  io1ii  49503  iscnrm3lem4  49518  iscnrm3r  49530  setrec1lem4  50272  aacllem  50383