Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30485 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  5534  sess2  5590  wefrc  5618  wereu2  5621  predtrss  6280  frpomin  6298  funun  6538  ssimaex  6919  f1cofveqaeq  7205  f1imass  7212  soisoi  7276  isores3  7283  isofrlem  7288  isoselem  7289  weniso  7302  abnexg  7703  oninton  7742  orduniorsuc  7774  limuni3  7796  tfindsg  7805  limom  7826  resf1extb  7878  f1o2ndf1  8065  soxp  8072  xpord3inddlem  8097  soseq  8102  extmptsuppeq  8131  smoel  8293  tfrlem9  8317  tz7.49  8377  seqomlem1  8382  odi  8507  omass  8508  omeulem2  8511  oeordsuc  8523  oeeulem  8530  naddsuc2  8630  ertr  8652  swoord2  8670  ecopovtrn  8760  domtriord  9054  pssnn  9096  unxpdomlem2  9160  isinf  9168  f1finf1o  9176  findcard3  9186  frfi  9188  unblem3  9197  supssd  9369  infssd  9400  en3lplem1  9524  inf3lem5  9544  cantnfle  9583  cantnfp1lem3  9592  ttrcltr  9628  frmin  9664  rankxpsuc  9797  tcrank  9799  ficardom  9876  carduni  9896  infxpenlem  9926  dfac8alem  9942  ac10ct  9947  ween  9948  alephdom  9994  alephle  10001  iscard3  10006  alephfp  10021  pwsdompw  10116  infdif  10121  cfslbn  10180  cofsmo  10182  cfcof  10187  fin1a2s  10327  domtriomlem  10355  ac6num  10392  zorn2lem3  10411  axdclem2  10433  imadomg  10447  iundom2g  10453  ficard  10478  fpwwe2lem7  10551  fpwwe2  10557  gchpwdom  10584  gchaclem  10592  tskr1om2  10682  inar1  10689  tskord  10694  tskuni  10697  grudomon  10731  grur1a  10733  grur1  10734  addnidpi  10815  ltexnq  10889  genpnnp  10919  addclprlem2  10931  mulclprlem  10933  psslinpr  10945  ltexprlem6  10955  ltexprlem7  10956  addcanpr  10960  mulgt0sr  11019  map2psrpr  11024  supsrlem  11025  axrrecex  11077  letr  11231  dedekind  11300  recex  11773  lemul12b  12003  mulgt1OLD  12005  fimaxre2  12092  lbreu  12097  nnrecgt0  12211  nnunb  12424  bndndx  12427  zeo  12606  uzind  12612  fzind  12618  fnn0ind  12619  suprfinzcl  12634  suprzcl2  12879  zmax  12886  rpnnen1lem5  12922  xrletr  13100  qbtwnre  13142  qsqueeze  13144  qextltlem  13145  xralrple  13148  xlesubadd  13206  supxrunb1  13262  icoshft  13417  zltaddlt1le  13449  fzen  13486  elfz0fzfz0  13578  elfzmlbp  13584  elfzo0z  13647  fzofzim  13655  fzo1fzo0n0  13661  elfzodifsumelfzo  13677  ssfzoulel  13706  modadd1  13858  modmul1  13877  uzrdgfni  13911  fsuppmapnn0fiub0  13946  fsuppmapnn0ub  13948  fsuppmapnn0fz  13949  seqf1olem1  13994  seqf1olem2  13995  expnbnd  14185  faclbnd4lem4  14249  hashgt23el  14377  seqcoll  14417  hashle2pr  14430  elss2prb  14441  ccatalpha  14547  swrdsbslen  14618  swrdspsleq  14619  swrdswrdlem  14657  swrdswrd  14658  pfxccatin12lem2a  14680  pfxccatin12lem1  14681  pfxccatin12lem3  14685  swrdccat3blem  14692  reuccatpfxs1lem  14699  repswswrd  14737  cshf1  14763  swrd2lsw  14905  sqeqd  15119  sqrmo  15204  cau3lem  15308  icodiamlt  15391  limsupbnd2  15436  lo1bdd2  15477  climuni  15505  rlimcn3  15543  mulcn2  15549  o1of2  15566  rlimo1  15570  lo1le  15605  iseralt  15638  cvgrat  15839  fprodss  15904  rpnnen2lem12  16183  ruclem3  16191  sqrt2irr  16207  p1modz1  16219  dvdsmodexp  16220  dvds2lem  16228  dvdslelem  16269  dvdsabseq  16273  divalglem8  16360  bitsinv1lem  16401  sadcaddlem  16417  smu01lem  16445  smueqlem  16450  bezoutlem4  16502  dfgcd2  16506  algcvga  16539  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfdvdsb  16603  coprmgcdb  16609  coprmdvds2  16614  coprmprod  16621  isprm3  16643  prmdvdsfz  16666  isprm5  16668  coprm  16672  rpexp12i  16685  phibndlem  16731  dfphi2  16735  eulerthlem2  16743  odzdvds  16757  iserodd  16797  pclem  16800  pcpremul  16805  pcqcl  16818  pcdvdsb  16831  pcprmpw2  16844  difsqpwdvds  16849  pcaddlem  16850  pcmptcl  16853  pcfac  16861  prmpwdvds  16866  unbenlem  16870  prmreclem1  16878  4sqlem17  16923  vdwmc2  16941  vdwlem9  16951  vdwlem10  16952  vdwlem13  16955  vdwnnlem3  16959  ramcl  16991  prmgaplem7  17019  mreiincl  17549  initoid  17959  termoid  17960  initoeu2lem1  17972  pospo  18300  resspos  18386  resstos  18387  dirge  18560  cyccom  19169  gsmsymgrfixlem1  19393  oddvdsnn0  19510  oddvds  19513  odcl2  19531  gexdvds  19550  sylow2alem2  19584  sylow2a  19585  efgi2  19691  efgsrel  19700  efgs1b  19702  imasabl  19842  cyggex2  19863  telgsums  19959  pgpfac1lem2  20043  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfac1lem5  20047  zrtermorngc  20611  zrtermoringc  20643  lmodfopnelem2  20885  lssssr  20940  rnglidlmcl  21206  gzrngunitlem  21422  znunit  21553  frgpcyg  21563  lsmcss  21682  obselocv  21718  obslbs  21720  mhpvarcl  22124  cply1mul  22271  gsummoncoe1  22283  cpmatacl  22691  cpmatinvcl  22692  cpmatmcllem  22693  m2cpminvid2lem  22729  mp2pm2mplem4  22784  pm2mp  22800  chfacfisf  22829  chfacfisfcpmat  22830  chfacfscmul0  22833  chfacfpmmul0  22837  cayhamlem4  22863  ordtrest2lem  23178  leordtval2  23187  lecldbas  23194  cncls  23249  cncnp  23255  cnpresti  23263  lmcnp  23279  cnt0  23321  isreg2  23352  cmpsublem  23374  cmpsub  23375  tgcmp  23376  bwth  23385  dfconn2  23394  1stcfb  23420  1stcelcls  23436  islly2  23459  dislly  23472  reftr  23489  comppfsc  23507  kgencn2  23532  txcnp  23595  txindis  23609  txcmplem1  23616  txlm  23623  xkohaus  23628  cnmptcom  23653  kqfvima  23705  isr0  23712  fgss2  23849  fbasrn  23859  filuni  23860  ufilmax  23882  isufil2  23883  cfinufil  23903  fmfnfmlem1  23929  fmfnfmlem2  23930  fmfnfmlem4  23932  fmfnfm  23933  fmco  23936  flimopn  23950  hausflim  23956  flimrest  23958  fclsopn  23989  flimfnfcls  24003  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALT  24026  ptcmplem2  24028  cnextcn  24042  symgtgp  24081  qustgplem  24096  tsmsres  24119  tsmsxplem1  24128  isucn2  24253  imasdsf1olem  24348  bldisj  24373  blssps  24399  blss  24400  metcnp3  24515  ngptgp  24611  nrginvrcn  24667  nmoleub  24706  xrsmopn  24788  icccmplem3  24800  reconnlem2  24803  rectbntr0  24808  rescncf  24874  iocopnst  24917  iccpnfcnv  24921  lebnumii  24943  nmoleub2lem  25091  nmhmcn  25097  iscfil3  25250  iscau2  25254  iscau3  25255  iscau4  25256  iscmet3lem2  25269  caussi  25274  equivcfil  25276  equivcau  25277  ivthlem2  25429  ivthlem3  25430  ovoliunlem2  25480  ovoliunnul  25484  ioombl1lem4  25538  dyadmax  25575  dyadmbl  25577  volsup2  25582  itg2le  25716  itg2const2  25718  itg2seq  25719  itgsplitioo  25815  rolle  25967  c1lip1  25974  dvivthlem1  25985  lhop1  25991  dvcnvrelem1  25994  dvfsumrlim  26008  ply1divmo  26111  ig1peu  26150  plypf1  26187  coeaddlem  26224  dvply2g  26261  fta1  26285  quotcan  26286  aalioulem4  26312  ulmcaulem  26372  ulmcn  26377  pilem2  26430  sincosq1lem  26474  sinq12gt0  26484  sinq12ge0  26485  tanord1  26514  lognegb  26567  logrec  26740  logbgcd1irr  26771  dcubic  26823  xrlimcnp  26945  o1cxp  26952  ftalem2  27051  ftalem3  27052  fsumdvdscom  27162  chtub  27189  vmasum  27193  bcmono  27254  bposlem3  27263  bposlem7  27267  lgsdir  27309  lgsqrlem2  27324  lgsqrmodndvds  27330  gausslemma2dlem6  27349  gausslemma2d  27351  lgsquadlem2  27358  2lgslem3a1  27377  2lgslem3b1  27378  2lgslem3c1  27379  2lgslem3d1  27380  2sqlem6  27400  2sq2  27410  2sqmod  27413  dchrisumlem3  27468  pntrsumbnd2  27544  pntpbnd1  27563  pntibnd  27570  pntlem3  27586  pntleml  27588  ltsres  27640  nosepon  27643  nolesgn2o  27649  nogesgn1o  27651  nodenselem8  27669  nosupbnd1lem1  27686  madess  27872  madebdaylemlrcut  27905  peano5uzs  28410  bdayfinbndlem1  28473  z12bday  28491  brbtwn2  28988  colinearalg  28993  axcontlem10  29056  edgupgr  29217  edglnl  29226  usgruspgrb  29266  subupgr  29370  uhgrspan1  29386  usgredgsscusgredg  29543  fusgrn0degnn0  29583  upgrewlkle2  29690  uspgr2wlkeq  29729  redwlk  29754  wlkdlem2  29765  upgrwlkdvdelem  29819  pthdlem1  29849  pthdlem2  29851  crctcshwlkn0lem3  29895  wlkiswwlks1  29950  wwlksm1edg  29964  wwlksnred  29975  wwlksnextbi  29977  umgr2adedgspth  30031  clwlkclwwlklem2fv2  30081  clwlkclwwlklem2a  30083  clwlkclwwlkf1lem3  30091  clwwisshclwwslemlem  30098  clwwlkf  30132  clwwlkext2edg  30141  wwlksubclwwlk  30143  clwwlknonex2lem2  30193  eupth2lems  30323  frgrwopreglem4a  30395  frgrregorufrg  30411  ex-natded5.3-2  30493  isgrpo  30583  vacn  30780  ubthlem2  30957  htthlem  31003  normgt0  31213  shmodsi  31475  spansneleq  31656  h1datomi  31667  nmcexi  32112  pjnormssi  32254  stm1add3i  32333  golem2  32358  cvnsym  32376  dmdmd  32386  mdslmd1lem1  32411  mdslmd1i  32415  mdexchi  32421  atcveq0  32434  superpos  32440  hatomistici  32448  atoml2i  32469  atcvat2i  32473  chirredlem1  32476  atcvat3i  32482  mdsymlem3  32491  mdsymlem5  32493  cdj3lem2b  32523  cdj3i  32527  submarchi  33262  dfufd2  33625  tpr2rico  34072  ordtrest2NEWlem  34082  xrge0iifcnv  34093  omssubadd  34460  eulerpartlemb  34528  ballotlemfc0  34653  ballotlemfcc  34654  ftc2re  34758  fissorduni  35249  fineqvinfep  35285  loop1cycl  35335  subfacp1lem6  35383  iccllysconn  35448  cvmfolem  35477  satfsschain  35562  satfrel  35565  satfdm  35567  sat1el2xp  35577  satffunlem1lem1  35600  dmopab3rexdif  35603  satffunlem2lem2  35604  satffun  35607  fundmpss  35965  dfon2lem3  35981  dfon2lem6  35984  axextbdist  35996  dfrdg4  36149  5segofs  36204  cgrextend  36206  segconeu  36209  btwncomim  36211  btwnswapid  36215  btwnintr  36217  btwnexch3  36218  btwndiff  36225  ifscgr  36242  cgrxfr  36253  btwnxfr  36254  lineext  36274  brofs2  36275  linecgr  36279  lineid  36281  idinside  36282  endofsegid  36283  btwnconn1lem13  36297  btwnconn3  36301  finminlem  36516  nn0prpwlem  36520  cldbnd  36524  clsint2  36527  fnessref  36555  neibastop3  36560  fgmin  36568  onsuct0  36639  limsucncmpi  36643  tr0elw  36682  tr0el  36683  bj-nnfea  37047  bj-axc14  37179  bj-restn0  37418  bj-0int  37429  wl-19.2reqv  37863  wl-aetr  37868  wl-axc11r  37869  fin2so  37942  tan2h  37947  lindsenlbs  37950  poimirlem2  37957  poimirlem9  37964  poimirlem17  37972  poimirlem18  37973  poimirlem21  37976  poimirlem23  37978  poimirlem26  37981  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimir  37988  heicant  37990  mblfinlem2  37993  mblfinlem3  37994  itg2addnclem  38006  itg2addnclem2  38007  itg2gt0cn  38010  ftc1anclem5  38032  ftc1anclem6  38033  filbcmb  38075  nninfnub  38086  mettrifi  38092  geomcau  38094  istotbnd3  38106  sstotbnd2  38109  ismtybndlem  38141  heibor1lem  38144  heiborlem1  38146  heiborlem8  38153  heiborlem10  38155  heibor  38156  opidonOLD  38187  riscer  38323  crngohomfo  38341  keridl  38367  ispridl2  38373  ispridlc  38405  ac6s6  38507  eqvreltr  39026  eldisjdmqsim  39152  suceldisj  39153  eldisjs6  39275  dral1-o  39364  ax12indalem  39405  ax12inda2ALT  39406  lsatcveq0  39492  eqlkr3  39561  atlatmstc  39779  atlrelat1  39781  hlrelat2  39863  intnatN  39867  cvrexchlem  39879  cvratlem  39881  cvrat2  39889  atltcvr  39895  cvrat3  39902  cvrat4  39903  ps-1  39937  ps-2  39938  lplnnle2at  40001  lvolnle3at  40042  2llnma3r  40248  cdlemblem  40253  pmapjoin  40312  elpcliN  40353  lhpmcvr4N  40486  4atexlemnclw  40530  trlnidatb  40637  cdlemc4  40654  cdlemd3  40660  cdleme3g  40694  cdleme7d  40706  cdleme11c  40721  cdleme11dN  40722  cdleme21b  40786  cdleme21c  40787  cdleme21i  40795  cdleme22b  40801  cdleme35fnpq  40909  cdlemf1  41021  trlord  41029  cdlemg6c  41080  dihglblem6  41800  dochlkr  41845  dochkrshp  41846  dihjat1lem  41888  dochexmidlem5  41924  dochexmidlem8  41927  qsalrel  42694  remulcand  42885  prjspner1  43073  fphpdo  43263  pellexlem5  43279  pellexlem6  43280  jm2.26lem3  43447  unxpwdom3  43541  omlimcl2  43688  oe0suclim  43723  cantnfresb  43770  tfsconcatb0  43790  naddgeoa  43840  iscard5  43981  sqrtcval  44086  ov2ssiunov2  44145  frege124d  44206  ordpss  44895  19.41rg  44995  relpfrlem  45398  modelaxreplem2  45424  stoweidlem34  46480  ormklocald  47320  evenwodadd  47333  cfsetsnfsetf1  47519  fcoresf1  47529  euoreqb  47569  2reu8i  47573  ralralimp  47738  f1oresf1o2  47751  zm1nn  47762  elfz2z  47775  2tceilhalfelfzo1  47796  m1modmmod  47824  modlt0b  47829  muldvdsfacgt  47846  muldvdsfacm1  47847  iccpartlt  47896  iccelpart  47905  icceuelpartlem  47907  fargshiftf1  47913  sprsymrelf1lem  47963  paireqne  47983  reuopreuprim  47998  goldbachthlem2  48021  odz2prm2pw  48038  fmtnoprmfac1lem  48039  fmtnofac2lem  48043  prmdvdsfmtnof1  48062  sfprmdvdsmersenne  48078  lighneallem2  48081  lighneallem4  48085  fppr2odd  48219  gbegt5  48249  gbowge7  48251  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgoldbach  48305  grimuhgr  48375  grimcnv  48376  grimco  48377  isuspgrim0  48382  isuspgrimlem  48383  upgrimwlklem5  48389  upgrimtrlslem2  48393  uhgrimisgrgriclem  48418  clnbgrgrimlem  48421  clnbgrgrim  48422  grimedg  48423  grtriprop  48429  isubgr3stgrlem3  48456  isubgr3stgrlem4  48457  isubgr3stgrlem6  48459  isubgr3stgrlem7  48460  uspgrlimlem3  48478  grlimedgclnbgr  48483  grlimgrtrilem2  48490  grlimgrtri  48491  grlicsym  48501  gpgedgvtx1  48550  gpgedgiov  48553  gpgedg2ov  48554  gpgedg2iv  48555  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  lcosslsp  48926  lindslinindsimp1  48945  snlindsntor  48959  itcovalt2  49165  eenglngeehlnmlem2  49226  itsclc0yqsol  49252  itschlc0xyqsol1  49254  itschlc0xyqsol  49255  opnneilv  49396  i0oii  49407  io1ii  49408  iscnrm3lem4  49423  iscnrm3r  49435  setrec1lem4  50177  aacllem  50288