Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30378 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  603  animpimp2impd  846  ax12v2  2182  alrimdd  2217  axc16g  2263  axc16nf  2266  axc11r  2368  sb4a  2480  2eu1  2646  2eu1v  2647  ss2ralv  4005  ss2rexv  4006  trel3  5207  poss  5526  sess2  5582  wefrc  5610  wereu2  5613  predtrss  6269  frpomin  6287  funun  6527  ssimaex  6907  f1cofveqaeq  7191  f1imass  7198  soisoi  7262  isores3  7269  isofrlem  7274  isoselem  7275  weniso  7288  abnexg  7689  oninton  7728  orduniorsuc  7760  limuni3  7782  tfindsg  7791  limom  7812  resf1extb  7864  f1o2ndf1  8052  soxp  8059  xpord3inddlem  8084  soseq  8089  extmptsuppeq  8118  smoel  8280  tfrlem9  8304  tz7.49  8364  seqomlem1  8369  odi  8494  omass  8495  omeulem2  8498  oeordsuc  8509  oeeulem  8516  naddsuc2  8616  ertr  8637  swoord2  8655  ecopovtrn  8744  domtriord  9036  pssnn  9078  unxpdomlem2  9141  isinf  9149  f1finf1o  9157  findcard3  9167  frfi  9169  unblem3  9178  supssd  9347  infssd  9378  en3lplem1  9502  inf3lem5  9522  cantnfle  9561  cantnfp1lem3  9570  ttrcltr  9606  frmin  9642  rankxpsuc  9775  tcrank  9777  ficardom  9854  carduni  9874  infxpenlem  9904  dfac8alem  9920  ac10ct  9925  ween  9926  alephdom  9972  alephle  9979  iscard3  9984  alephfp  9999  pwsdompw  10094  infdif  10099  cfslbn  10158  cofsmo  10160  cfcof  10165  fin1a2s  10305  domtriomlem  10333  ac6num  10370  zorn2lem3  10389  axdclem2  10411  imadomg  10425  iundom2g  10431  ficard  10456  fpwwe2lem7  10528  fpwwe2  10534  gchpwdom  10561  gchaclem  10569  tskr1om2  10659  inar1  10666  tskord  10671  tskuni  10674  grudomon  10708  grur1a  10710  grur1  10711  addnidpi  10792  ltexnq  10866  genpnnp  10896  addclprlem2  10908  mulclprlem  10910  psslinpr  10922  ltexprlem6  10932  ltexprlem7  10933  addcanpr  10937  mulgt0sr  10996  map2psrpr  11001  supsrlem  11002  axrrecex  11054  letr  11207  dedekind  11276  recex  11749  lemul12b  11978  mulgt1OLD  11980  fimaxre2  12067  lbreu  12072  nnrecgt0  12168  nnunb  12377  bndndx  12380  zeo  12559  uzind  12565  fzind  12571  fnn0ind  12572  suprfinzcl  12587  suprzcl2  12836  zmax  12843  rpnnen1lem5  12879  xrletr  13057  qbtwnre  13098  qsqueeze  13100  qextltlem  13101  xralrple  13104  xlesubadd  13162  supxrunb1  13218  icoshft  13373  zltaddlt1le  13405  fzen  13441  elfz0fzfz0  13533  elfzmlbp  13539  elfzo0z  13601  fzofzim  13609  fzo1fzo0n0  13615  elfzodifsumelfzo  13631  ssfzoulel  13660  modadd1  13812  modmul1  13831  uzrdgfni  13865  fsuppmapnn0fiub0  13900  fsuppmapnn0ub  13902  fsuppmapnn0fz  13903  seqf1olem1  13948  seqf1olem2  13949  expnbnd  14139  faclbnd4lem4  14203  hashgt23el  14331  seqcoll  14371  hashle2pr  14384  elss2prb  14395  ccatalpha  14501  swrdsbslen  14572  swrdspsleq  14573  swrdswrdlem  14611  swrdswrd  14612  pfxccatin12lem2a  14634  pfxccatin12lem1  14635  pfxccatin12lem3  14639  swrdccat3blem  14646  reuccatpfxs1lem  14653  repswswrd  14691  cshf1  14717  swrd2lsw  14859  sqeqd  15073  sqrmo  15158  cau3lem  15262  icodiamlt  15345  limsupbnd2  15390  lo1bdd2  15431  climuni  15459  rlimcn3  15497  mulcn2  15503  o1of2  15520  rlimo1  15524  lo1le  15559  iseralt  15592  cvgrat  15790  fprodss  15855  rpnnen2lem12  16134  ruclem3  16142  sqrt2irr  16158  p1modz1  16170  dvdsmodexp  16171  dvds2lem  16179  dvdslelem  16220  dvdsabseq  16224  divalglem8  16311  bitsinv1lem  16352  sadcaddlem  16368  smu01lem  16396  smueqlem  16401  bezoutlem4  16453  dfgcd2  16457  algcvga  16490  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfdvdsb  16554  coprmgcdb  16560  coprmdvds2  16565  coprmprod  16572  isprm3  16594  prmdvdsfz  16616  isprm5  16618  coprm  16622  rpexp12i  16635  phibndlem  16681  dfphi2  16685  eulerthlem2  16693  odzdvds  16707  iserodd  16747  pclem  16750  pcpremul  16755  pcqcl  16768  pcdvdsb  16781  pcprmpw2  16794  difsqpwdvds  16799  pcaddlem  16800  pcmptcl  16803  pcfac  16811  prmpwdvds  16816  unbenlem  16820  prmreclem1  16828  4sqlem17  16873  vdwmc2  16891  vdwlem9  16901  vdwlem10  16902  vdwlem13  16905  vdwnnlem3  16909  ramcl  16941  prmgaplem7  16969  mreiincl  17498  initoid  17908  termoid  17909  initoeu2lem1  17921  pospo  18249  resspos  18335  resstos  18336  dirge  18509  cyccom  19116  gsmsymgrfixlem1  19340  oddvdsnn0  19457  oddvds  19460  odcl2  19478  gexdvds  19497  sylow2alem2  19531  sylow2a  19532  efgi2  19638  efgsrel  19647  efgs1b  19649  imasabl  19789  cyggex2  19810  telgsums  19906  pgpfac1lem2  19990  pgpfac1lem3a  19991  pgpfac1lem3  19992  pgpfac1lem5  19994  zrtermorngc  20559  zrtermoringc  20591  lmodfopnelem2  20833  lssssr  20888  rnglidlmcl  21154  gzrngunitlem  21370  znunit  21501  frgpcyg  21511  lsmcss  21630  obselocv  21666  obslbs  21668  mhpvarcl  22064  cply1mul  22212  gsummoncoe1  22224  cpmatacl  22632  cpmatinvcl  22633  cpmatmcllem  22634  m2cpminvid2lem  22670  mp2pm2mplem4  22725  pm2mp  22741  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmul0  22774  chfacfpmmul0  22778  cayhamlem4  22804  ordtrest2lem  23119  leordtval2  23128  lecldbas  23135  cncls  23190  cncnp  23196  cnpresti  23204  lmcnp  23220  cnt0  23262  isreg2  23293  cmpsublem  23315  cmpsub  23316  tgcmp  23317  bwth  23326  dfconn2  23335  1stcfb  23361  1stcelcls  23377  islly2  23400  dislly  23413  reftr  23430  comppfsc  23448  kgencn2  23473  txcnp  23536  txindis  23550  txcmplem1  23557  txlm  23564  xkohaus  23569  cnmptcom  23594  kqfvima  23646  isr0  23653  fgss2  23790  fbasrn  23800  filuni  23801  ufilmax  23823  isufil2  23824  cfinufil  23844  fmfnfmlem1  23870  fmfnfmlem2  23871  fmfnfmlem4  23873  fmfnfm  23874  fmco  23877  flimopn  23891  hausflim  23897  flimrest  23899  fclsopn  23930  flimfnfcls  23944  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALT  23967  ptcmplem2  23969  cnextcn  23983  symgtgp  24022  qustgplem  24037  tsmsres  24060  tsmsxplem1  24069  isucn2  24194  imasdsf1olem  24289  bldisj  24314  blssps  24340  blss  24341  metcnp3  24456  ngptgp  24552  nrginvrcn  24608  nmoleub  24647  xrsmopn  24729  icccmplem3  24741  reconnlem2  24744  rectbntr0  24749  rescncf  24818  iocopnst  24865  iccpnfcnv  24870  lebnumii  24893  nmoleub2lem  25042  nmhmcn  25048  iscfil3  25201  iscau2  25205  iscau3  25206  iscau4  25207  iscmet3lem2  25220  caussi  25225  equivcfil  25227  equivcau  25228  ivthlem2  25381  ivthlem3  25382  ovoliunlem2  25432  ovoliunnul  25436  ioombl1lem4  25490  dyadmax  25527  dyadmbl  25529  volsup2  25534  itg2le  25668  itg2const2  25670  itg2seq  25671  itgsplitioo  25767  rolle  25922  c1lip1  25930  dvivthlem1  25941  lhop1  25947  dvcnvrelem1  25950  dvfsumrlim  25966  ply1divmo  26069  ig1peu  26108  plypf1  26145  coeaddlem  26182  dvply2g  26220  fta1  26244  quotcan  26245  aalioulem4  26271  ulmcaulem  26331  ulmcn  26336  pilem2  26390  sincosq1lem  26434  sinq12gt0  26444  sinq12ge0  26445  tanord1  26474  lognegb  26527  logrec  26701  logbgcd1irr  26732  dcubic  26784  xrlimcnp  26906  o1cxp  26913  ftalem2  27012  ftalem3  27013  fsumdvdscom  27123  chtub  27151  vmasum  27155  bcmono  27216  bposlem3  27225  bposlem7  27229  lgsdir  27271  lgsqrlem2  27286  lgsqrmodndvds  27292  gausslemma2dlem6  27311  gausslemma2d  27313  lgsquadlem2  27320  2lgslem3a1  27339  2lgslem3b1  27340  2lgslem3c1  27341  2lgslem3d1  27342  2sqlem6  27362  2sq2  27372  2sqmod  27375  dchrisumlem3  27430  pntrsumbnd2  27506  pntpbnd1  27525  pntibnd  27532  pntlem3  27548  pntleml  27550  sltres  27602  nosepon  27605  nolesgn2o  27611  nogesgn1o  27613  nodenselem8  27631  nosupbnd1lem1  27648  madess  27822  madebdaylemlrcut  27845  peano5uzs  28329  brbtwn2  28884  colinearalg  28889  axcontlem10  28952  edgupgr  29113  edglnl  29122  usgruspgrb  29162  subupgr  29266  uhgrspan1  29282  usgredgsscusgredg  29439  fusgrn0degnn0  29479  upgrewlkle2  29586  uspgr2wlkeq  29625  redwlk  29650  wlkdlem2  29661  upgrwlkdvdelem  29715  pthdlem1  29745  pthdlem2  29747  crctcshwlkn0lem3  29791  wlkiswwlks1  29846  wwlksm1edg  29860  wwlksnred  29871  wwlksnextbi  29873  umgr2adedgspth  29927  clwlkclwwlklem2fv2  29974  clwlkclwwlklem2a  29976  clwlkclwwlkf1lem3  29984  clwwisshclwwslemlem  29991  clwwlkf  30025  clwwlkext2edg  30034  wwlksubclwwlk  30036  clwwlknonex2lem2  30086  eupth2lems  30216  frgrwopreglem4a  30288  frgrregorufrg  30304  ex-natded5.3-2  30386  isgrpo  30475  vacn  30672  ubthlem2  30849  htthlem  30895  normgt0  31105  shmodsi  31367  spansneleq  31548  h1datomi  31559  nmcexi  32004  pjnormssi  32146  stm1add3i  32225  golem2  32250  cvnsym  32268  dmdmd  32278  mdslmd1lem1  32303  mdslmd1i  32307  mdexchi  32313  atcveq0  32326  superpos  32332  hatomistici  32340  atoml2i  32361  atcvat2i  32365  chirredlem1  32368  atcvat3i  32374  mdsymlem3  32383  mdsymlem5  32385  cdj3lem2b  32415  cdj3i  32419  submarchi  33153  dfufd2  33513  tpr2rico  33923  ordtrest2NEWlem  33933  xrge0iifcnv  33944  omssubadd  34311  eulerpartlemb  34379  ballotlemfc0  34504  ballotlemfcc  34505  ftc2re  34609  fissorduni  35099  loop1cycl  35179  subfacp1lem6  35227  iccllysconn  35292  cvmfolem  35321  satfsschain  35406  satfrel  35409  satfdm  35411  sat1el2xp  35421  satffunlem1lem1  35444  dmopab3rexdif  35447  satffunlem2lem2  35448  satffun  35451  fundmpss  35809  dfon2lem3  35825  dfon2lem6  35828  axextbdist  35840  dfrdg4  35991  5segofs  36046  cgrextend  36048  segconeu  36051  btwncomim  36053  btwnswapid  36057  btwnintr  36059  btwnexch3  36060  btwndiff  36067  ifscgr  36084  cgrxfr  36095  btwnxfr  36096  lineext  36116  brofs2  36117  linecgr  36121  lineid  36123  idinside  36124  endofsegid  36125  btwnconn1lem13  36139  btwnconn3  36143  finminlem  36358  nn0prpwlem  36362  cldbnd  36366  clsint2  36369  fnessref  36397  neibastop3  36402  fgmin  36410  onsuct0  36481  limsucncmpi  36485  bj-nnfea  36774  bj-axc14  36896  bj-restn0  37130  bj-0int  37141  wl-19.2reqv  37564  wl-aetr  37569  wl-axc11r  37570  fin2so  37653  tan2h  37658  lindsenlbs  37661  poimirlem2  37668  poimirlem9  37675  poimirlem17  37683  poimirlem18  37684  poimirlem21  37687  poimirlem23  37689  poimirlem26  37692  poimirlem29  37695  poimirlem30  37696  poimirlem31  37697  poimir  37699  heicant  37701  mblfinlem2  37704  mblfinlem3  37705  itg2addnclem  37717  itg2addnclem2  37718  itg2gt0cn  37721  ftc1anclem5  37743  ftc1anclem6  37744  filbcmb  37786  nninfnub  37797  mettrifi  37803  geomcau  37805  istotbnd3  37817  sstotbnd2  37820  ismtybndlem  37852  heibor1lem  37855  heiborlem1  37857  heiborlem8  37864  heiborlem10  37866  heibor  37867  opidonOLD  37898  riscer  38034  crngohomfo  38052  keridl  38078  ispridl2  38084  ispridlc  38116  ac6s6  38218  eqvreltr  38650  dral1-o  38949  ax12indalem  38990  ax12inda2ALT  38991  lsatcveq0  39077  eqlkr3  39146  atlatmstc  39364  atlrelat1  39366  hlrelat2  39448  intnatN  39452  cvrexchlem  39464  cvratlem  39466  cvrat2  39474  atltcvr  39480  cvrat3  39487  cvrat4  39488  ps-1  39522  ps-2  39523  lplnnle2at  39586  lvolnle3at  39627  2llnma3r  39833  cdlemblem  39838  pmapjoin  39897  elpcliN  39938  lhpmcvr4N  40071  4atexlemnclw  40115  trlnidatb  40222  cdlemc4  40239  cdlemd3  40245  cdleme3g  40279  cdleme7d  40291  cdleme11c  40306  cdleme11dN  40307  cdleme21b  40371  cdleme21c  40372  cdleme21i  40380  cdleme22b  40386  cdleme35fnpq  40494  cdlemf1  40606  trlord  40614  cdlemg6c  40665  dihglblem6  41385  dochlkr  41430  dochkrshp  41431  dihjat1lem  41473  dochexmidlem5  41509  dochexmidlem8  41512  qsalrel  42279  remulcand  42478  prjspner1  42665  fphpdo  42856  pellexlem5  42872  pellexlem6  42873  jm2.26lem3  43040  unxpwdom3  43134  omlimcl2  43281  oe0suclim  43316  cantnfresb  43363  tfsconcatb0  43383  naddgeoa  43433  iscard5  43575  sqrtcval  43680  ov2ssiunov2  43739  frege124d  43800  ordpss  44489  19.41rg  44589  relpfrlem  44992  modelaxreplem2  45018  stoweidlem34  46078  ormklocald  46918  evenwodadd  46922  cfsetsnfsetf1  47096  fcoresf1  47106  euoreqb  47146  2reu8i  47150  ralralimp  47315  f1oresf1o2  47328  zm1nn  47339  elfz2z  47352  2tceilhalfelfzo1  47369  m1modmmod  47395  modlt0b  47400  iccpartlt  47461  iccelpart  47470  icceuelpartlem  47472  fargshiftf1  47478  sprsymrelf1lem  47528  paireqne  47548  reuopreuprim  47563  goldbachthlem2  47583  odz2prm2pw  47600  fmtnoprmfac1lem  47601  fmtnofac2lem  47605  prmdvdsfmtnof1  47624  sfprmdvdsmersenne  47640  lighneallem2  47643  lighneallem4  47647  fppr2odd  47768  gbegt5  47798  gbowge7  47800  bgoldbtbndlem4  47845  bgoldbtbnd  47846  tgoldbach  47854  grimuhgr  47924  grimcnv  47925  grimco  47926  isuspgrim0  47931  isuspgrimlem  47932  upgrimwlklem5  47938  upgrimtrlslem2  47942  uhgrimisgrgriclem  47967  clnbgrgrimlem  47970  clnbgrgrim  47971  grimedg  47972  grtriprop  47978  isubgr3stgrlem3  48005  isubgr3stgrlem4  48006  isubgr3stgrlem6  48008  isubgr3stgrlem7  48009  uspgrlimlem3  48027  grlimedgclnbgr  48032  grlimgrtrilem2  48039  grlimgrtri  48040  grlicsym  48050  gpgedgvtx1  48099  gpgedgiov  48102  gpgedg2ov  48103  gpgedg2iv  48104  pgnioedg1  48145  pgnioedg2  48146  pgnioedg3  48147  pgnioedg4  48148  pgnioedg5  48149  pgnbgreunbgrlem2lem1  48151  pgnbgreunbgrlem2lem2  48152  pgnbgreunbgrlem2lem3  48153  pgnbgreunbgrlem5lem1  48157  pgnbgreunbgrlem5lem2  48158  pgnbgreunbgrlem5lem3  48159  lcosslsp  48476  lindslinindsimp1  48495  snlindsntor  48509  itcovalt2  48715  eenglngeehlnmlem2  48776  itsclc0yqsol  48802  itschlc0xyqsol1  48804  itschlc0xyqsol  48805  opnneilv  48946  i0oii  48957  io1ii  48958  iscnrm3lem4  48973  iscnrm3r  48985  setrec1lem4  49728  aacllem  49839