Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30329 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  2180  alrimdd  2215  axc16g  2261  axc16nf  2264  axc11r  2366  sb4a  2478  2eu1  2644  2eu1v  2645  ss2ralv  4017  ss2rexv  4018  trel3  5224  poss  5548  sess2  5604  wefrc  5632  wereu2  5635  predtrss  6295  frpomin  6313  funun  6562  ssimaex  6946  f1cofveqaeq  7232  f1imass  7239  soisoi  7303  isores3  7310  isofrlem  7315  isoselem  7316  weniso  7329  abnexg  7732  oninton  7771  orduniorsuc  7805  limuni3  7828  tfindsg  7837  limom  7858  resf1extb  7910  f1o2ndf1  8101  soxp  8108  xpord3inddlem  8133  soseq  8138  extmptsuppeq  8167  smoel  8329  tfrlem9  8353  tz7.49  8413  seqomlem1  8418  odi  8543  omass  8544  omeulem2  8547  oeordsuc  8558  oeeulem  8565  naddsuc2  8665  ertr  8686  swoord2  8704  ecopovtrn  8793  domtriord  9087  pssnn  9132  unxpdomlem2  9198  isinf  9207  isinfOLD  9208  f1finf1o  9216  findcard3  9229  findcard3OLD  9230  frfi  9232  unblem3  9241  supssd  9414  infssd  9445  en3lplem1  9565  inf3lem5  9585  cantnfle  9624  cantnfp1lem3  9633  ttrcltr  9669  frmin  9702  rankxpsuc  9835  tcrank  9837  ficardom  9914  carduni  9934  infxpenlem  9966  dfac8alem  9982  ac10ct  9987  ween  9988  alephdom  10034  alephle  10041  iscard3  10046  alephfp  10061  pwsdompw  10156  infdif  10161  cfslbn  10220  cofsmo  10222  cfcof  10227  fin1a2s  10367  domtriomlem  10395  ac6num  10432  zorn2lem3  10451  axdclem2  10473  imadomg  10487  iundom2g  10493  ficard  10518  fpwwe2lem7  10590  fpwwe2  10596  gchpwdom  10623  gchaclem  10631  tskr1om2  10721  inar1  10728  tskord  10733  tskuni  10736  grudomon  10770  grur1a  10772  grur1  10773  addnidpi  10854  ltexnq  10928  genpnnp  10958  addclprlem2  10970  mulclprlem  10972  psslinpr  10984  ltexprlem6  10994  ltexprlem7  10995  addcanpr  10999  mulgt0sr  11058  map2psrpr  11063  supsrlem  11064  axrrecex  11116  letr  11268  dedekind  11337  recex  11810  lemul12b  12039  mulgt1OLD  12041  fimaxre2  12128  lbreu  12133  nnrecgt0  12229  nnunb  12438  bndndx  12441  zeo  12620  uzind  12626  fzind  12632  fnn0ind  12633  suprfinzcl  12648  suprzcl2  12897  zmax  12904  rpnnen1lem5  12940  xrletr  13118  qbtwnre  13159  qsqueeze  13161  qextltlem  13162  xralrple  13165  xlesubadd  13223  supxrunb1  13279  icoshft  13434  zltaddlt1le  13466  fzen  13502  elfz0fzfz0  13594  elfzmlbp  13600  elfzo0z  13662  fzofzim  13670  fzo1fzo0n0  13676  elfzodifsumelfzo  13692  ssfzoulel  13721  modadd1  13870  modmul1  13889  uzrdgfni  13923  fsuppmapnn0fiub0  13958  fsuppmapnn0ub  13960  fsuppmapnn0fz  13961  seqf1olem1  14006  seqf1olem2  14007  expnbnd  14197  faclbnd4lem4  14261  hashgt23el  14389  seqcoll  14429  hashle2pr  14442  elss2prb  14453  ccatalpha  14558  swrdsbslen  14629  swrdspsleq  14630  swrdswrdlem  14669  swrdswrd  14670  pfxccatin12lem2a  14692  pfxccatin12lem1  14693  pfxccatin12lem3  14697  swrdccat3blem  14704  reuccatpfxs1lem  14711  repswswrd  14749  cshf1  14775  swrd2lsw  14918  sqeqd  15132  sqrmo  15217  cau3lem  15321  icodiamlt  15404  limsupbnd2  15449  lo1bdd2  15490  climuni  15518  rlimcn3  15556  mulcn2  15562  o1of2  15579  rlimo1  15583  lo1le  15618  iseralt  15651  cvgrat  15849  fprodss  15914  rpnnen2lem12  16193  ruclem3  16201  sqrt2irr  16217  p1modz1  16229  dvdsmodexp  16230  dvds2lem  16238  dvdslelem  16279  dvdsabseq  16283  divalglem8  16370  bitsinv1lem  16411  sadcaddlem  16427  smu01lem  16455  smueqlem  16460  bezoutlem4  16512  dfgcd2  16516  algcvga  16549  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfdvdsb  16613  coprmgcdb  16619  coprmdvds2  16624  coprmprod  16631  isprm3  16653  prmdvdsfz  16675  isprm5  16677  coprm  16681  rpexp12i  16694  phibndlem  16740  dfphi2  16744  eulerthlem2  16752  odzdvds  16766  iserodd  16806  pclem  16809  pcpremul  16814  pcqcl  16827  pcdvdsb  16840  pcprmpw2  16853  difsqpwdvds  16858  pcaddlem  16859  pcmptcl  16862  pcfac  16870  prmpwdvds  16875  unbenlem  16879  prmreclem1  16887  4sqlem17  16932  vdwmc2  16950  vdwlem9  16960  vdwlem10  16961  vdwlem13  16964  vdwnnlem3  16968  ramcl  17000  prmgaplem7  17028  mreiincl  17557  initoid  17963  termoid  17964  initoeu2lem1  17976  pospo  18304  dirge  18562  cyccom  19135  gsmsymgrfixlem1  19357  oddvdsnn0  19474  oddvds  19477  odcl2  19495  gexdvds  19514  sylow2alem2  19548  sylow2a  19549  efgi2  19655  efgsrel  19664  efgs1b  19666  imasabl  19806  cyggex2  19827  telgsums  19923  pgpfac1lem2  20007  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfac1lem5  20011  zrtermorngc  20552  zrtermoringc  20584  lmodfopnelem2  20805  lssssr  20860  rnglidlmcl  21126  gzrngunitlem  21349  znunit  21473  frgpcyg  21483  lsmcss  21601  obselocv  21637  obslbs  21639  mhpvarcl  22035  cply1mul  22183  gsummoncoe1  22195  cpmatacl  22603  cpmatinvcl  22604  cpmatmcllem  22605  m2cpminvid2lem  22641  mp2pm2mplem4  22696  pm2mp  22712  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmul0  22745  chfacfpmmul0  22749  cayhamlem4  22775  ordtrest2lem  23090  leordtval2  23099  lecldbas  23106  cncls  23161  cncnp  23167  cnpresti  23175  lmcnp  23191  cnt0  23233  isreg2  23264  cmpsublem  23286  cmpsub  23287  tgcmp  23288  bwth  23297  dfconn2  23306  1stcfb  23332  1stcelcls  23348  islly2  23371  dislly  23384  reftr  23401  comppfsc  23419  kgencn2  23444  txcnp  23507  txindis  23521  txcmplem1  23528  txlm  23535  xkohaus  23540  cnmptcom  23565  kqfvima  23617  isr0  23624  fgss2  23761  fbasrn  23771  filuni  23772  ufilmax  23794  isufil2  23795  cfinufil  23815  fmfnfmlem1  23841  fmfnfmlem2  23842  fmfnfmlem4  23844  fmfnfm  23845  fmco  23848  flimopn  23862  hausflim  23868  flimrest  23870  fclsopn  23901  flimfnfcls  23915  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALT  23938  ptcmplem2  23940  cnextcn  23954  symgtgp  23993  qustgplem  24008  tsmsres  24031  tsmsxplem1  24040  isucn2  24166  imasdsf1olem  24261  bldisj  24286  blssps  24312  blss  24313  metcnp3  24428  ngptgp  24524  nrginvrcn  24580  nmoleub  24619  xrsmopn  24701  icccmplem3  24713  reconnlem2  24716  rectbntr0  24721  rescncf  24790  iocopnst  24837  iccpnfcnv  24842  lebnumii  24865  nmoleub2lem  25014  nmhmcn  25020  iscfil3  25173  iscau2  25177  iscau3  25178  iscau4  25179  iscmet3lem2  25192  caussi  25197  equivcfil  25199  equivcau  25200  ivthlem2  25353  ivthlem3  25354  ovoliunlem2  25404  ovoliunnul  25408  ioombl1lem4  25462  dyadmax  25499  dyadmbl  25501  volsup2  25506  itg2le  25640  itg2const2  25642  itg2seq  25643  itgsplitioo  25739  rolle  25894  c1lip1  25902  dvivthlem1  25913  lhop1  25919  dvcnvrelem1  25922  dvfsumrlim  25938  ply1divmo  26041  ig1peu  26080  plypf1  26117  coeaddlem  26154  dvply2g  26192  fta1  26216  quotcan  26217  aalioulem4  26243  ulmcaulem  26303  ulmcn  26308  pilem2  26362  sincosq1lem  26406  sinq12gt0  26416  sinq12ge0  26417  tanord1  26446  lognegb  26499  logrec  26673  logbgcd1irr  26704  dcubic  26756  xrlimcnp  26878  o1cxp  26885  ftalem2  26984  ftalem3  26985  fsumdvdscom  27095  chtub  27123  vmasum  27127  bcmono  27188  bposlem3  27197  bposlem7  27201  lgsdir  27243  lgsqrlem2  27258  lgsqrmodndvds  27264  gausslemma2dlem6  27283  gausslemma2d  27285  lgsquadlem2  27292  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  2sqlem6  27334  2sq2  27344  2sqmod  27347  dchrisumlem3  27402  pntrsumbnd2  27478  pntpbnd1  27497  pntibnd  27504  pntlem3  27520  pntleml  27522  sltres  27574  nosepon  27577  nolesgn2o  27583  nogesgn1o  27585  nodenselem8  27603  nosupbnd1lem1  27620  madess  27788  madebdaylemlrcut  27810  peano5uzs  28292  brbtwn2  28832  colinearalg  28837  axcontlem10  28900  edgupgr  29061  edglnl  29070  usgruspgrb  29110  subupgr  29214  uhgrspan1  29230  usgredgsscusgredg  29387  fusgrn0degnn0  29427  upgrewlkle2  29534  uspgr2wlkeq  29574  redwlk  29600  wlkdlem2  29611  upgrwlkdvdelem  29666  pthdlem1  29696  pthdlem2  29698  crctcshwlkn0lem3  29742  wlkiswwlks1  29797  wwlksm1edg  29811  wwlksnred  29822  wwlksnextbi  29824  umgr2adedgspth  29878  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a  29927  clwlkclwwlkf1lem3  29935  clwwisshclwwslemlem  29942  clwwlkf  29976  clwwlkext2edg  29985  wwlksubclwwlk  29987  clwwlknonex2lem2  30037  eupth2lems  30167  frgrwopreglem4a  30239  frgrregorufrg  30255  ex-natded5.3-2  30337  isgrpo  30426  vacn  30623  ubthlem2  30800  htthlem  30846  normgt0  31056  shmodsi  31318  spansneleq  31499  h1datomi  31510  nmcexi  31955  pjnormssi  32097  stm1add3i  32176  golem2  32201  cvnsym  32219  dmdmd  32229  mdslmd1lem1  32254  mdslmd1i  32258  mdexchi  32264  atcveq0  32277  superpos  32283  hatomistici  32291  atoml2i  32312  atcvat2i  32316  chirredlem1  32319  atcvat3i  32325  mdsymlem3  32334  mdsymlem5  32336  cdj3lem2b  32366  cdj3i  32370  resspos  32892  resstos  32893  submarchi  33140  dfufd2  33521  tpr2rico  33902  ordtrest2NEWlem  33912  xrge0iifcnv  33923  omssubadd  34291  eulerpartlemb  34359  ballotlemfc0  34484  ballotlemfcc  34485  ftc2re  34589  loop1cycl  35124  subfacp1lem6  35172  iccllysconn  35237  cvmfolem  35266  satfsschain  35351  satfrel  35354  satfdm  35356  sat1el2xp  35366  satffunlem1lem1  35389  dmopab3rexdif  35392  satffunlem2lem2  35393  satffun  35396  fundmpss  35754  dfon2lem3  35773  dfon2lem6  35776  axextbdist  35788  dfrdg4  35939  5segofs  35994  cgrextend  35996  segconeu  35999  btwncomim  36001  btwnswapid  36005  btwnintr  36007  btwnexch3  36008  btwndiff  36015  ifscgr  36032  cgrxfr  36043  btwnxfr  36044  lineext  36064  brofs2  36065  linecgr  36069  lineid  36071  idinside  36072  endofsegid  36073  btwnconn1lem13  36087  btwnconn3  36091  finminlem  36306  nn0prpwlem  36310  cldbnd  36314  clsint2  36317  fnessref  36345  neibastop3  36350  fgmin  36358  onsuct0  36429  limsucncmpi  36433  bj-nnfea  36722  bj-axc14  36844  bj-restn0  37078  bj-0int  37089  wl-19.2reqv  37512  wl-aetr  37517  wl-axc11r  37518  fin2so  37601  tan2h  37606  lindsenlbs  37609  poimirlem2  37616  poimirlem9  37623  poimirlem17  37631  poimirlem18  37632  poimirlem21  37635  poimirlem23  37637  poimirlem26  37640  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimir  37647  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  itg2addnclem  37665  itg2addnclem2  37666  itg2gt0cn  37669  ftc1anclem5  37691  ftc1anclem6  37692  filbcmb  37734  nninfnub  37745  mettrifi  37751  geomcau  37753  istotbnd3  37765  sstotbnd2  37768  ismtybndlem  37800  heibor1lem  37803  heiborlem1  37805  heiborlem8  37812  heiborlem10  37814  heibor  37815  opidonOLD  37846  riscer  37982  crngohomfo  38000  keridl  38026  ispridl2  38032  ispridlc  38064  ac6s6  38166  eqvreltr  38598  dral1-o  38897  ax12indalem  38938  ax12inda2ALT  38939  lsatcveq0  39025  eqlkr3  39094  atlatmstc  39312  atlrelat1  39314  hlrelat2  39397  intnatN  39401  cvrexchlem  39413  cvratlem  39415  cvrat2  39423  atltcvr  39429  cvrat3  39436  cvrat4  39437  ps-1  39471  ps-2  39472  lplnnle2at  39535  lvolnle3at  39576  2llnma3r  39782  cdlemblem  39787  pmapjoin  39846  elpcliN  39887  lhpmcvr4N  40020  4atexlemnclw  40064  trlnidatb  40171  cdlemc4  40188  cdlemd3  40194  cdleme3g  40228  cdleme7d  40240  cdleme11c  40255  cdleme11dN  40256  cdleme21b  40320  cdleme21c  40321  cdleme21i  40329  cdleme22b  40335  cdleme35fnpq  40443  cdlemf1  40555  trlord  40563  cdlemg6c  40614  dihglblem6  41334  dochlkr  41379  dochkrshp  41380  dihjat1lem  41422  dochexmidlem5  41458  dochexmidlem8  41461  qsalrel  42228  remulcand  42427  prjspner1  42614  fphpdo  42805  pellexlem5  42821  pellexlem6  42822  jm2.26lem3  42990  unxpwdom3  43084  omlimcl2  43231  oe0suclim  43266  cantnfresb  43313  tfsconcatb0  43333  naddgeoa  43383  iscard5  43525  sqrtcval  43630  ov2ssiunov2  43689  frege124d  43750  ordpss  44440  19.41rg  44540  relpfrlem  44943  modelaxreplem2  44969  stoweidlem34  46032  ormklocald  46872  evenwodadd  46886  cfsetsnfsetf1  47060  fcoresf1  47070  euoreqb  47110  2reu8i  47114  ralralimp  47279  f1oresf1o2  47292  zm1nn  47303  elfz2z  47316  2tceilhalfelfzo1  47333  m1modmmod  47359  modlt0b  47364  iccpartlt  47425  iccelpart  47434  icceuelpartlem  47436  fargshiftf1  47442  sprsymrelf1lem  47492  paireqne  47512  reuopreuprim  47527  goldbachthlem2  47547  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnofac2lem  47569  prmdvdsfmtnof1  47588  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem4  47611  fppr2odd  47732  gbegt5  47762  gbowge7  47764  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgoldbach  47818  grimuhgr  47887  grimcnv  47888  grimco  47889  isuspgrim0  47894  isuspgrimlem  47895  upgrimwlklem5  47901  upgrimtrlslem2  47905  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933  clnbgrgrim  47934  grimedg  47935  grtriprop  47940  isubgr3stgrlem3  47967  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  uspgrlimlem3  47989  grlimgrtrilem2  47994  grlimgrtri  47995  grlicsym  48005  gpgedgvtx1  48053  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  lcosslsp  48427  lindslinindsimp1  48446  snlindsntor  48460  itcovalt2  48666  eenglngeehlnmlem2  48727  itsclc0yqsol  48753  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  opnneilv  48897  i0oii  48908  io1ii  48909  iscnrm3lem4  48924  iscnrm3r  48936  setrec1lem4  49679  aacllem  49790