Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30490 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  179  sylibd  239  sylbid  240  sylibrd  259  sylbird  260  syland  604  animpimp2impd  847  ax12v2  2187  alrimdd  2222  axc16g  2268  axc16nf  2271  axc11r  2373  sb4a  2485  2eu1  2652  2eu1v  2653  ss2ralv  3993  ss2rexv  3994  trel3  5202  poss  5532  sess2  5588  wefrc  5616  wereu2  5619  predtrss  6278  frpomin  6296  funun  6536  ssimaex  6917  f1cofveqaeq  7203  f1imass  7210  soisoi  7274  isores3  7281  isofrlem  7286  isoselem  7287  weniso  7300  abnexg  7701  oninton  7740  orduniorsuc  7772  limuni3  7794  tfindsg  7803  limom  7824  resf1extb  7876  f1o2ndf1  8063  soxp  8070  xpord3inddlem  8095  soseq  8100  extmptsuppeq  8129  smoel  8291  tfrlem9  8315  tz7.49  8375  seqomlem1  8380  odi  8505  omass  8506  omeulem2  8509  oeordsuc  8521  oeeulem  8528  naddsuc2  8628  ertr  8650  swoord2  8668  ecopovtrn  8758  domtriord  9052  pssnn  9094  unxpdomlem2  9158  isinf  9166  f1finf1o  9174  findcard3  9184  frfi  9186  unblem3  9195  supssd  9367  infssd  9398  en3lplem1  9522  inf3lem5  9542  cantnfle  9581  cantnfp1lem3  9590  ttrcltr  9626  frmin  9662  rankxpsuc  9795  tcrank  9797  ficardom  9874  carduni  9894  infxpenlem  9924  dfac8alem  9940  ac10ct  9945  ween  9946  alephdom  9992  alephle  9999  iscard3  10004  alephfp  10019  pwsdompw  10114  infdif  10119  cfslbn  10178  cofsmo  10180  cfcof  10185  fin1a2s  10325  domtriomlem  10353  ac6num  10390  zorn2lem3  10409  axdclem2  10431  imadomg  10445  iundom2g  10451  ficard  10476  fpwwe2lem7  10549  fpwwe2  10555  gchpwdom  10582  gchaclem  10590  tskr1om2  10680  inar1  10687  tskord  10692  tskuni  10695  grudomon  10729  grur1a  10731  grur1  10732  addnidpi  10813  ltexnq  10887  genpnnp  10917  addclprlem2  10929  mulclprlem  10931  psslinpr  10943  ltexprlem6  10953  ltexprlem7  10954  addcanpr  10958  mulgt0sr  11017  map2psrpr  11022  supsrlem  11023  axrrecex  11075  letr  11229  dedekind  11298  recex  11771  lemul12b  12001  mulgt1OLD  12003  fimaxre2  12090  lbreu  12095  nnrecgt0  12209  nnunb  12422  bndndx  12425  zeo  12604  uzind  12610  fzind  12616  fnn0ind  12617  suprfinzcl  12632  suprzcl2  12877  zmax  12884  rpnnen1lem5  12920  xrletr  13098  qbtwnre  13140  qsqueeze  13142  qextltlem  13143  xralrple  13146  xlesubadd  13204  supxrunb1  13260  icoshft  13415  zltaddlt1le  13447  fzen  13484  elfz0fzfz0  13576  elfzmlbp  13582  elfzo0z  13645  fzofzim  13653  fzo1fzo0n0  13659  elfzodifsumelfzo  13675  ssfzoulel  13704  modadd1  13856  modmul1  13875  uzrdgfni  13909  fsuppmapnn0fiub0  13944  fsuppmapnn0ub  13946  fsuppmapnn0fz  13947  seqf1olem1  13992  seqf1olem2  13993  expnbnd  14183  faclbnd4lem4  14247  hashgt23el  14375  seqcoll  14415  hashle2pr  14428  elss2prb  14439  ccatalpha  14545  swrdsbslen  14616  swrdspsleq  14617  swrdswrdlem  14655  swrdswrd  14656  pfxccatin12lem2a  14678  pfxccatin12lem1  14679  pfxccatin12lem3  14683  swrdccat3blem  14690  reuccatpfxs1lem  14697  repswswrd  14735  cshf1  14761  swrd2lsw  14903  sqeqd  15117  sqrmo  15202  cau3lem  15306  icodiamlt  15389  limsupbnd2  15434  lo1bdd2  15475  climuni  15503  rlimcn3  15541  mulcn2  15547  o1of2  15564  rlimo1  15568  lo1le  15603  iseralt  15636  cvgrat  15837  fprodss  15902  rpnnen2lem12  16181  ruclem3  16189  sqrt2irr  16205  p1modz1  16217  dvdsmodexp  16218  dvds2lem  16226  dvdslelem  16267  dvdsabseq  16271  divalglem8  16358  bitsinv1lem  16399  sadcaddlem  16415  smu01lem  16443  smueqlem  16448  bezoutlem4  16500  dfgcd2  16504  algcvga  16537  lcmfunsnlem1  16595  lcmfunsnlem2lem1  16596  lcmfunsnlem2lem2  16597  lcmfdvdsb  16601  coprmgcdb  16607  coprmdvds2  16612  coprmprod  16619  isprm3  16641  prmdvdsfz  16664  isprm5  16666  coprm  16670  rpexp12i  16683  phibndlem  16729  dfphi2  16733  eulerthlem2  16741  odzdvds  16755  iserodd  16795  pclem  16798  pcpremul  16803  pcqcl  16816  pcdvdsb  16829  pcprmpw2  16842  difsqpwdvds  16847  pcaddlem  16848  pcmptcl  16851  pcfac  16859  prmpwdvds  16864  unbenlem  16868  prmreclem1  16876  4sqlem17  16921  vdwmc2  16939  vdwlem9  16949  vdwlem10  16950  vdwlem13  16953  vdwnnlem3  16957  ramcl  16989  prmgaplem7  17017  mreiincl  17547  initoid  17957  termoid  17958  initoeu2lem1  17970  pospo  18298  resspos  18384  resstos  18385  dirge  18558  cyccom  19167  gsmsymgrfixlem1  19391  oddvdsnn0  19508  oddvds  19511  odcl2  19529  gexdvds  19548  sylow2alem2  19582  sylow2a  19583  efgi2  19689  efgsrel  19698  efgs1b  19700  imasabl  19840  cyggex2  19861  telgsums  19957  pgpfac1lem2  20041  pgpfac1lem3a  20042  pgpfac1lem3  20043  pgpfac1lem5  20045  zrtermorngc  20609  zrtermoringc  20641  lmodfopnelem2  20883  lssssr  20938  rnglidlmcl  21204  gzrngunitlem  21420  znunit  21551  frgpcyg  21561  lsmcss  21680  obselocv  21716  obslbs  21718  mhpvarcl  22123  cply1mul  22270  gsummoncoe1  22282  cpmatacl  22690  cpmatinvcl  22691  cpmatmcllem  22692  m2cpminvid2lem  22728  mp2pm2mplem4  22783  pm2mp  22799  chfacfisf  22828  chfacfisfcpmat  22829  chfacfscmul0  22832  chfacfpmmul0  22836  cayhamlem4  22862  ordtrest2lem  23177  leordtval2  23186  lecldbas  23193  cncls  23248  cncnp  23254  cnpresti  23262  lmcnp  23278  cnt0  23320  isreg2  23351  cmpsublem  23373  cmpsub  23374  tgcmp  23375  bwth  23384  dfconn2  23393  1stcfb  23419  1stcelcls  23435  islly2  23458  dislly  23471  reftr  23488  comppfsc  23506  kgencn2  23531  txcnp  23594  txindis  23608  txcmplem1  23615  txlm  23622  xkohaus  23627  cnmptcom  23652  kqfvima  23704  isr0  23711  fgss2  23848  fbasrn  23858  filuni  23859  ufilmax  23881  isufil2  23882  cfinufil  23902  fmfnfmlem1  23928  fmfnfmlem2  23929  fmfnfmlem4  23931  fmfnfm  23932  fmco  23935  flimopn  23949  hausflim  23955  flimrest  23957  fclsopn  23988  flimfnfcls  24002  alexsubALTlem2  24022  alexsubALTlem3  24023  alexsubALT  24025  ptcmplem2  24027  cnextcn  24041  symgtgp  24080  qustgplem  24095  tsmsres  24118  tsmsxplem1  24127  isucn2  24252  imasdsf1olem  24347  bldisj  24372  blssps  24398  blss  24399  metcnp3  24514  ngptgp  24610  nrginvrcn  24666  nmoleub  24705  xrsmopn  24787  icccmplem3  24799  reconnlem2  24802  rectbntr0  24807  rescncf  24873  iocopnst  24916  iccpnfcnv  24920  lebnumii  24942  nmoleub2lem  25090  nmhmcn  25096  iscfil3  25249  iscau2  25253  iscau3  25254  iscau4  25255  iscmet3lem2  25268  caussi  25273  equivcfil  25275  equivcau  25276  ivthlem2  25428  ivthlem3  25429  ovoliunlem2  25479  ovoliunnul  25483  ioombl1lem4  25537  dyadmax  25574  dyadmbl  25576  volsup2  25581  itg2le  25715  itg2const2  25717  itg2seq  25718  itgsplitioo  25814  rolle  25966  c1lip1  25974  dvivthlem1  25985  lhop1  25991  dvcnvrelem1  25994  dvfsumrlim  26010  ply1divmo  26113  ig1peu  26152  plypf1  26189  coeaddlem  26226  dvply2g  26263  fta1  26287  quotcan  26288  aalioulem4  26314  ulmcaulem  26374  ulmcn  26379  pilem2  26433  sincosq1lem  26477  sinq12gt0  26487  sinq12ge0  26488  tanord1  26517  lognegb  26570  logrec  26744  logbgcd1irr  26775  dcubic  26827  xrlimcnp  26949  o1cxp  26956  ftalem2  27055  ftalem3  27056  fsumdvdscom  27166  chtub  27194  vmasum  27198  bcmono  27259  bposlem3  27268  bposlem7  27272  lgsdir  27314  lgsqrlem2  27329  lgsqrmodndvds  27335  gausslemma2dlem6  27354  gausslemma2d  27356  lgsquadlem2  27363  2lgslem3a1  27382  2lgslem3b1  27383  2lgslem3c1  27384  2lgslem3d1  27385  2sqlem6  27405  2sq2  27415  2sqmod  27418  dchrisumlem3  27473  pntrsumbnd2  27549  pntpbnd1  27568  pntibnd  27575  pntlem3  27591  pntleml  27593  ltsres  27645  nosepon  27648  nolesgn2o  27654  nogesgn1o  27656  nodenselem8  27674  nosupbnd1lem1  27691  madess  27877  madebdaylemlrcut  27910  peano5uzs  28415  bdayfinbndlem1  28478  z12bday  28496  brbtwn2  28993  colinearalg  28998  axcontlem10  29061  edgupgr  29222  edglnl  29231  usgruspgrb  29271  subupgr  29375  uhgrspan1  29391  usgredgsscusgredg  29548  fusgrn0degnn0  29588  upgrewlkle2  29695  uspgr2wlkeq  29734  redwlk  29759  wlkdlem2  29770  upgrwlkdvdelem  29824  pthdlem1  29854  pthdlem2  29856  crctcshwlkn0lem3  29900  wlkiswwlks1  29955  wwlksm1edg  29969  wwlksnred  29980  wwlksnextbi  29982  umgr2adedgspth  30036  clwlkclwwlklem2fv2  30086  clwlkclwwlklem2a  30088  clwlkclwwlkf1lem3  30096  clwwisshclwwslemlem  30103  clwwlkf  30137  clwwlkext2edg  30146  wwlksubclwwlk  30148  clwwlknonex2lem2  30198  eupth2lems  30328  frgrwopreglem4a  30400  frgrregorufrg  30416  ex-natded5.3-2  30498  isgrpo  30588  vacn  30785  ubthlem2  30962  htthlem  31008  normgt0  31218  shmodsi  31480  spansneleq  31661  h1datomi  31672  nmcexi  32117  pjnormssi  32259  stm1add3i  32338  golem2  32363  cvnsym  32381  dmdmd  32391  mdslmd1lem1  32416  mdslmd1i  32420  mdexchi  32426  atcveq0  32439  superpos  32445  hatomistici  32453  atoml2i  32474  atcvat2i  32478  chirredlem1  32481  atcvat3i  32487  mdsymlem3  32496  mdsymlem5  32498  cdj3lem2b  32528  cdj3i  32532  submarchi  33267  dfufd2  33630  tpr2rico  34077  ordtrest2NEWlem  34087  xrge0iifcnv  34098  omssubadd  34465  eulerpartlemb  34533  ballotlemfc0  34658  ballotlemfcc  34659  ftc2re  34763  fissorduni  35254  fineqvinfep  35290  loop1cycl  35340  subfacp1lem6  35388  iccllysconn  35453  cvmfolem  35482  satfsschain  35567  satfrel  35570  satfdm  35572  sat1el2xp  35582  satffunlem1lem1  35605  dmopab3rexdif  35608  satffunlem2lem2  35609  satffun  35612  fundmpss  35970  dfon2lem3  35986  dfon2lem6  35989  axextbdist  36001  dfrdg4  36154  5segofs  36209  cgrextend  36211  segconeu  36214  btwncomim  36216  btwnswapid  36220  btwnintr  36222  btwnexch3  36223  btwndiff  36230  ifscgr  36247  cgrxfr  36258  btwnxfr  36259  lineext  36279  brofs2  36280  linecgr  36284  lineid  36286  idinside  36287  endofsegid  36288  btwnconn1lem13  36302  btwnconn3  36306  finminlem  36521  nn0prpwlem  36525  cldbnd  36529  clsint2  36532  fnessref  36560  neibastop3  36565  fgmin  36573  onsuct0  36644  limsucncmpi  36648  tr0elw  36687  tr0el  36688  bj-nnfea  37044  bj-axc14  37176  bj-restn0  37415  bj-0int  37426  wl-19.2reqv  37860  wl-aetr  37865  wl-axc11r  37866  fin2so  37939  tan2h  37944  lindsenlbs  37947  poimirlem2  37954  poimirlem9  37961  poimirlem17  37969  poimirlem18  37970  poimirlem21  37973  poimirlem23  37975  poimirlem26  37978  poimirlem29  37981  poimirlem30  37982  poimirlem31  37983  poimir  37985  heicant  37987  mblfinlem2  37990  mblfinlem3  37991  itg2addnclem  38003  itg2addnclem2  38004  itg2gt0cn  38007  ftc1anclem5  38029  ftc1anclem6  38030  filbcmb  38072  nninfnub  38083  mettrifi  38089  geomcau  38091  istotbnd3  38103  sstotbnd2  38106  ismtybndlem  38138  heibor1lem  38141  heiborlem1  38143  heiborlem8  38150  heiborlem10  38152  heibor  38153  opidonOLD  38184  riscer  38320  crngohomfo  38338  keridl  38364  ispridl2  38370  ispridlc  38402  ac6s6  38504  eqvreltr  39023  eldisjdmqsim  39149  suceldisj  39150  eldisjs6  39272  dral1-o  39361  ax12indalem  39402  ax12inda2ALT  39403  lsatcveq0  39489  eqlkr3  39558  atlatmstc  39776  atlrelat1  39778  hlrelat2  39860  intnatN  39864  cvrexchlem  39876  cvratlem  39878  cvrat2  39886  atltcvr  39892  cvrat3  39899  cvrat4  39900  ps-1  39934  ps-2  39935  lplnnle2at  39998  lvolnle3at  40039  2llnma3r  40245  cdlemblem  40250  pmapjoin  40309  elpcliN  40350  lhpmcvr4N  40483  4atexlemnclw  40527  trlnidatb  40634  cdlemc4  40651  cdlemd3  40657  cdleme3g  40691  cdleme7d  40703  cdleme11c  40718  cdleme11dN  40719  cdleme21b  40783  cdleme21c  40784  cdleme21i  40792  cdleme22b  40798  cdleme35fnpq  40906  cdlemf1  41018  trlord  41026  cdlemg6c  41077  dihglblem6  41797  dochlkr  41842  dochkrshp  41843  dihjat1lem  41885  dochexmidlem5  41921  dochexmidlem8  41924  qsalrel  42691  remulcand  42882  prjspner1  43070  fphpdo  43260  pellexlem5  43276  pellexlem6  43277  jm2.26lem3  43444  unxpwdom3  43538  omlimcl2  43685  oe0suclim  43720  cantnfresb  43767  tfsconcatb0  43787  naddgeoa  43837  iscard5  43978  sqrtcval  44083  ov2ssiunov2  44142  frege124d  44203  ordpss  44892  19.41rg  44992  relpfrlem  45395  modelaxreplem2  45421  stoweidlem34  46477  ormklocald  47317  evenwodadd  47330  cfsetsnfsetf1  47504  fcoresf1  47514  euoreqb  47554  2reu8i  47558  ralralimp  47723  f1oresf1o2  47736  zm1nn  47747  elfz2z  47760  2tceilhalfelfzo1  47781  m1modmmod  47809  modlt0b  47814  muldvdsfacgt  47831  muldvdsfacm1  47832  iccpartlt  47881  iccelpart  47890  icceuelpartlem  47892  fargshiftf1  47898  sprsymrelf1lem  47948  paireqne  47968  reuopreuprim  47983  goldbachthlem2  48006  odz2prm2pw  48023  fmtnoprmfac1lem  48024  fmtnofac2lem  48028  prmdvdsfmtnof1  48047  sfprmdvdsmersenne  48063  lighneallem2  48066  lighneallem4  48070  fppr2odd  48204  gbegt5  48234  gbowge7  48236  bgoldbtbndlem4  48281  bgoldbtbnd  48282  tgoldbach  48290  grimuhgr  48360  grimcnv  48361  grimco  48362  isuspgrim0  48367  isuspgrimlem  48368  upgrimwlklem5  48374  upgrimtrlslem2  48378  uhgrimisgrgriclem  48403  clnbgrgrimlem  48406  clnbgrgrim  48407  grimedg  48408  grtriprop  48414  isubgr3stgrlem3  48441  isubgr3stgrlem4  48442  isubgr3stgrlem6  48444  isubgr3stgrlem7  48445  uspgrlimlem3  48463  grlimedgclnbgr  48468  grlimgrtrilem2  48475  grlimgrtri  48476  grlicsym  48486  gpgedgvtx1  48535  gpgedgiov  48538  gpgedg2ov  48539  gpgedg2iv  48540  pgnioedg1  48581  pgnioedg2  48582  pgnioedg3  48583  pgnioedg4  48584  pgnioedg5  48585  pgnbgreunbgrlem2lem1  48587  pgnbgreunbgrlem2lem2  48588  pgnbgreunbgrlem2lem3  48589  pgnbgreunbgrlem5lem1  48593  pgnbgreunbgrlem5lem2  48594  pgnbgreunbgrlem5lem3  48595  lcosslsp  48911  lindslinindsimp1  48930  snlindsntor  48944  itcovalt2  49150  eenglngeehlnmlem2  49211  itsclc0yqsol  49237  itschlc0xyqsol1  49239  itschlc0xyqsol  49240  opnneilv  49381  i0oii  49392  io1ii  49393  iscnrm3lem4  49408  iscnrm3r  49420  setrec1lem4  50162  aacllem  50273