Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30386 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  2371  sb4a  2485  2eu1  2651  2eu1v  2652  ss2ralv  4034  ss2rexv  4035  trel3  5244  poss  5568  sess2  5625  wefrc  5653  wereu2  5656  predtrss  6316  frpomin  6334  funun  6587  ssimaex  6969  f1cofveqaeq  7255  f1imass  7262  soisoi  7326  isores3  7333  isofrlem  7338  isoselem  7339  weniso  7352  abnexg  7755  oninton  7794  orduniorsuc  7829  limuni3  7852  tfindsg  7861  limom  7882  resf1extb  7935  f1o2ndf1  8126  soxp  8133  xpord3inddlem  8158  soseq  8163  extmptsuppeq  8192  smoel  8379  tfrlem9  8404  tz7.49  8464  seqomlem1  8469  odi  8596  omass  8597  omeulem2  8600  oeordsuc  8611  oeeulem  8618  naddsuc2  8718  ertr  8739  swoord2  8757  ecopovtrn  8839  domtriord  9142  pssnn  9187  onomeneqOLD  9243  unxpdomlem2  9264  isinf  9273  isinfOLD  9274  f1finf1o  9282  findcard3  9295  findcard3OLD  9296  frfi  9298  unblem3  9307  supssd  9480  infssd  9511  en3lplem1  9631  inf3lem5  9651  cantnfle  9690  cantnfp1lem3  9699  ttrcltr  9735  frmin  9768  rankxpsuc  9901  tcrank  9903  ficardom  9980  carduni  10000  infxpenlem  10032  dfac8alem  10048  ac10ct  10053  ween  10054  alephdom  10100  alephle  10107  iscard3  10112  alephfp  10127  pwsdompw  10222  infdif  10227  cfslbn  10286  cofsmo  10288  cfcof  10293  fin1a2s  10433  domtriomlem  10461  ac6num  10498  zorn2lem3  10517  axdclem2  10539  imadomg  10553  iundom2g  10559  ficard  10584  fpwwe2lem7  10656  fpwwe2  10662  gchpwdom  10689  gchaclem  10697  tskr1om2  10787  inar1  10794  tskord  10799  tskuni  10802  grudomon  10836  grur1a  10838  grur1  10839  addnidpi  10920  ltexnq  10994  genpnnp  11024  addclprlem2  11036  mulclprlem  11038  psslinpr  11050  ltexprlem6  11060  ltexprlem7  11061  addcanpr  11065  mulgt0sr  11124  map2psrpr  11129  supsrlem  11130  axrrecex  11182  letr  11334  dedekind  11403  recex  11874  lemul12b  12103  mulgt1OLD  12105  fimaxre2  12192  lbreu  12197  nnrecgt0  12288  nnunb  12502  bndndx  12505  zeo  12684  uzind  12690  fzind  12696  fnn0ind  12697  suprfinzcl  12712  suprzcl2  12959  zmax  12966  rpnnen1lem5  13002  xrletr  13179  qbtwnre  13220  qsqueeze  13222  qextltlem  13223  xralrple  13226  xlesubadd  13284  supxrunb1  13340  icoshft  13495  zltaddlt1le  13527  fzen  13563  elfz0fzfz0  13655  elfzmlbp  13661  elfzo0z  13723  fzofzim  13731  fzo1fzo0n0  13736  elfzodifsumelfzo  13752  ssfzoulel  13781  modadd1  13930  modmul1  13947  uzrdgfni  13981  fsuppmapnn0fiub0  14016  fsuppmapnn0ub  14018  fsuppmapnn0fz  14019  seqf1olem1  14064  seqf1olem2  14065  expnbnd  14255  faclbnd4lem4  14319  hashgt23el  14447  seqcoll  14487  hashle2pr  14500  elss2prb  14511  ccatalpha  14616  swrdsbslen  14687  swrdspsleq  14688  swrdswrdlem  14727  swrdswrd  14728  pfxccatin12lem2a  14750  pfxccatin12lem1  14751  pfxccatin12lem3  14755  swrdccat3blem  14762  reuccatpfxs1lem  14769  repswswrd  14807  cshf1  14833  swrd2lsw  14976  sqeqd  15190  sqrmo  15275  cau3lem  15378  icodiamlt  15459  limsupbnd2  15504  lo1bdd2  15545  climuni  15573  rlimcn3  15611  mulcn2  15617  o1of2  15634  rlimo1  15638  lo1le  15673  iseralt  15706  cvgrat  15904  fprodss  15969  rpnnen2lem12  16248  ruclem3  16256  sqrt2irr  16272  p1modz1  16284  dvdsmodexp  16285  dvds2lem  16293  dvdslelem  16333  dvdsabseq  16337  divalglem8  16424  bitsinv1lem  16465  sadcaddlem  16481  smu01lem  16509  smueqlem  16514  bezoutlem4  16566  dfgcd2  16570  algcvga  16603  lcmfunsnlem1  16661  lcmfunsnlem2lem1  16662  lcmfunsnlem2lem2  16663  lcmfdvdsb  16667  coprmgcdb  16673  coprmdvds2  16678  coprmprod  16685  isprm3  16707  prmdvdsfz  16729  isprm5  16731  coprm  16735  rpexp12i  16748  phibndlem  16794  dfphi2  16798  eulerthlem2  16806  odzdvds  16820  iserodd  16860  pclem  16863  pcpremul  16868  pcqcl  16881  pcdvdsb  16894  pcprmpw2  16907  difsqpwdvds  16912  pcaddlem  16913  pcmptcl  16916  pcfac  16924  prmpwdvds  16929  unbenlem  16933  prmreclem1  16941  4sqlem17  16986  vdwmc2  17004  vdwlem9  17014  vdwlem10  17015  vdwlem13  17018  vdwnnlem3  17022  ramcl  17054  prmgaplem7  17082  mreiincl  17613  initoid  18019  termoid  18020  initoeu2lem1  18032  pospo  18360  dirge  18618  cyccom  19191  gsmsymgrfixlem1  19413  oddvdsnn0  19530  oddvds  19533  odcl2  19551  gexdvds  19570  sylow2alem2  19604  sylow2a  19605  efgi2  19711  efgsrel  19720  efgs1b  19722  imasabl  19862  cyggex2  19883  telgsums  19979  pgpfac1lem2  20063  pgpfac1lem3a  20064  pgpfac1lem3  20065  pgpfac1lem5  20067  zrtermorngc  20608  zrtermoringc  20640  lmodfopnelem2  20861  lssssr  20916  rnglidlmcl  21182  gzrngunitlem  21405  znunit  21529  frgpcyg  21539  lsmcss  21657  obselocv  21693  obslbs  21695  mhpvarcl  22091  cply1mul  22239  gsummoncoe1  22251  cpmatacl  22659  cpmatinvcl  22660  cpmatmcllem  22661  m2cpminvid2lem  22697  mp2pm2mplem4  22752  pm2mp  22768  chfacfisf  22797  chfacfisfcpmat  22798  chfacfscmul0  22801  chfacfpmmul0  22805  cayhamlem4  22831  ordtrest2lem  23146  leordtval2  23155  lecldbas  23162  cncls  23217  cncnp  23223  cnpresti  23231  lmcnp  23247  cnt0  23289  isreg2  23320  cmpsublem  23342  cmpsub  23343  tgcmp  23344  bwth  23353  dfconn2  23362  1stcfb  23388  1stcelcls  23404  islly2  23427  dislly  23440  reftr  23457  comppfsc  23475  kgencn2  23500  txcnp  23563  txindis  23577  txcmplem1  23584  txlm  23591  xkohaus  23596  cnmptcom  23621  kqfvima  23673  isr0  23680  fgss2  23817  fbasrn  23827  filuni  23828  ufilmax  23850  isufil2  23851  cfinufil  23871  fmfnfmlem1  23897  fmfnfmlem2  23898  fmfnfmlem4  23900  fmfnfm  23901  fmco  23904  flimopn  23918  hausflim  23924  flimrest  23926  fclsopn  23957  flimfnfcls  23971  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALT  23994  ptcmplem2  23996  cnextcn  24010  symgtgp  24049  qustgplem  24064  tsmsres  24087  tsmsxplem1  24096  isucn2  24222  imasdsf1olem  24317  bldisj  24342  blssps  24368  blss  24369  metcnp3  24484  ngptgp  24580  nrginvrcn  24636  nmoleub  24675  xrsmopn  24757  icccmplem3  24769  reconnlem2  24772  rectbntr0  24777  rescncf  24846  iocopnst  24893  iccpnfcnv  24898  lebnumii  24921  nmoleub2lem  25070  nmhmcn  25076  iscfil3  25230  iscau2  25234  iscau3  25235  iscau4  25236  iscmet3lem2  25249  caussi  25254  equivcfil  25256  equivcau  25257  ivthlem2  25410  ivthlem3  25411  ovoliunlem2  25461  ovoliunnul  25465  ioombl1lem4  25519  dyadmax  25556  dyadmbl  25558  volsup2  25563  itg2le  25697  itg2const2  25699  itg2seq  25700  itgsplitioo  25796  rolle  25951  c1lip1  25959  dvivthlem1  25970  lhop1  25976  dvcnvrelem1  25979  dvfsumrlim  25995  ply1divmo  26098  ig1peu  26137  plypf1  26174  coeaddlem  26211  dvply2g  26249  fta1  26273  quotcan  26274  aalioulem4  26300  ulmcaulem  26360  ulmcn  26365  pilem2  26419  sincosq1lem  26463  sinq12gt0  26473  sinq12ge0  26474  tanord1  26503  lognegb  26556  logrec  26730  logbgcd1irr  26761  dcubic  26813  xrlimcnp  26935  o1cxp  26942  ftalem2  27041  ftalem3  27042  fsumdvdscom  27152  chtub  27180  vmasum  27184  bcmono  27245  bposlem3  27254  bposlem7  27258  lgsdir  27300  lgsqrlem2  27315  lgsqrmodndvds  27321  gausslemma2dlem6  27340  gausslemma2d  27342  lgsquadlem2  27349  2lgslem3a1  27368  2lgslem3b1  27369  2lgslem3c1  27370  2lgslem3d1  27371  2sqlem6  27391  2sq2  27401  2sqmod  27404  dchrisumlem3  27459  pntrsumbnd2  27535  pntpbnd1  27554  pntibnd  27561  pntlem3  27577  pntleml  27579  sltres  27631  nosepon  27634  nolesgn2o  27640  nogesgn1o  27642  nodenselem8  27660  nosupbnd1lem1  27677  madess  27845  madebdaylemlrcut  27867  peano5uzs  28349  brbtwn2  28889  colinearalg  28894  axcontlem10  28957  edgupgr  29118  edglnl  29127  usgruspgrb  29167  subupgr  29271  uhgrspan1  29287  usgredgsscusgredg  29444  fusgrn0degnn0  29484  upgrewlkle2  29591  uspgr2wlkeq  29631  redwlk  29657  wlkdlem2  29668  upgrwlkdvdelem  29723  pthdlem1  29753  pthdlem2  29755  crctcshwlkn0lem3  29799  wlkiswwlks1  29854  wwlksm1edg  29868  wwlksnred  29879  wwlksnextbi  29881  umgr2adedgspth  29935  clwlkclwwlklem2fv2  29982  clwlkclwwlklem2a  29984  clwlkclwwlkf1lem3  29992  clwwisshclwwslemlem  29999  clwwlkf  30033  clwwlkext2edg  30042  wwlksubclwwlk  30044  clwwlknonex2lem2  30094  eupth2lems  30224  frgrwopreglem4a  30296  frgrregorufrg  30312  ex-natded5.3-2  30394  isgrpo  30483  vacn  30680  ubthlem2  30857  htthlem  30903  normgt0  31113  shmodsi  31375  spansneleq  31556  h1datomi  31567  nmcexi  32012  pjnormssi  32154  stm1add3i  32233  golem2  32258  cvnsym  32276  dmdmd  32286  mdslmd1lem1  32311  mdslmd1i  32315  mdexchi  32321  atcveq0  32334  superpos  32340  hatomistici  32348  atoml2i  32369  atcvat2i  32373  chirredlem1  32376  atcvat3i  32382  mdsymlem3  32391  mdsymlem5  32393  cdj3lem2b  32423  cdj3i  32427  resspos  32951  resstos  32952  submarchi  33189  dfufd2  33570  tpr2rico  33948  ordtrest2NEWlem  33958  xrge0iifcnv  33969  omssubadd  34337  eulerpartlemb  34405  ballotlemfc0  34530  ballotlemfcc  34531  ftc2re  34635  loop1cycl  35164  subfacp1lem6  35212  iccllysconn  35277  cvmfolem  35306  satfsschain  35391  satfrel  35394  satfdm  35396  sat1el2xp  35406  satffunlem1lem1  35429  dmopab3rexdif  35432  satffunlem2lem2  35433  satffun  35436  fundmpss  35789  dfon2lem3  35808  dfon2lem6  35811  axextbdist  35823  dfrdg4  35974  5segofs  36029  cgrextend  36031  segconeu  36034  btwncomim  36036  btwnswapid  36040  btwnintr  36042  btwnexch3  36043  btwndiff  36050  ifscgr  36067  cgrxfr  36078  btwnxfr  36079  lineext  36099  brofs2  36100  linecgr  36104  lineid  36106  idinside  36107  endofsegid  36108  btwnconn1lem13  36122  btwnconn3  36126  finminlem  36341  nn0prpwlem  36345  cldbnd  36349  clsint2  36352  fnessref  36380  neibastop3  36385  fgmin  36393  onsuct0  36464  limsucncmpi  36468  bj-nnfea  36757  bj-axc14  36879  bj-restn0  37113  bj-0int  37124  wl-19.2reqv  37547  wl-aetr  37552  wl-axc11r  37553  fin2so  37636  tan2h  37641  lindsenlbs  37644  poimirlem2  37651  poimirlem9  37658  poimirlem17  37666  poimirlem18  37667  poimirlem21  37670  poimirlem23  37672  poimirlem26  37675  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  poimir  37682  heicant  37684  mblfinlem2  37687  mblfinlem3  37688  itg2addnclem  37700  itg2addnclem2  37701  itg2gt0cn  37704  ftc1anclem5  37726  ftc1anclem6  37727  filbcmb  37769  nninfnub  37780  mettrifi  37786  geomcau  37788  istotbnd3  37800  sstotbnd2  37803  ismtybndlem  37835  heibor1lem  37838  heiborlem1  37840  heiborlem8  37847  heiborlem10  37849  heibor  37850  opidonOLD  37881  riscer  38017  crngohomfo  38035  keridl  38061  ispridl2  38067  ispridlc  38099  ac6s6  38201  eqvreltr  38630  dral1-o  38927  ax12indalem  38968  ax12inda2ALT  38969  lsatcveq0  39055  eqlkr3  39124  atlatmstc  39342  atlrelat1  39344  hlrelat2  39427  intnatN  39431  cvrexchlem  39443  cvratlem  39445  cvrat2  39453  atltcvr  39459  cvrat3  39466  cvrat4  39467  ps-1  39501  ps-2  39502  lplnnle2at  39565  lvolnle3at  39606  2llnma3r  39812  cdlemblem  39817  pmapjoin  39876  elpcliN  39917  lhpmcvr4N  40050  4atexlemnclw  40094  trlnidatb  40201  cdlemc4  40218  cdlemd3  40224  cdleme3g  40258  cdleme7d  40270  cdleme11c  40285  cdleme11dN  40286  cdleme21b  40350  cdleme21c  40351  cdleme21i  40359  cdleme22b  40365  cdleme35fnpq  40473  cdlemf1  40585  trlord  40593  cdlemg6c  40644  dihglblem6  41364  dochlkr  41409  dochkrshp  41410  dihjat1lem  41452  dochexmidlem5  41488  dochexmidlem8  41491  qsalrel  42258  remulcand  42456  prjspner1  42624  fphpdo  42815  pellexlem5  42831  pellexlem6  42832  jm2.26lem3  43000  unxpwdom3  43094  omlimcl2  43241  oe0suclim  43276  cantnfresb  43323  tfsconcatb0  43343  naddgeoa  43393  iscard5  43535  sqrtcval  43640  ov2ssiunov2  43699  frege124d  43760  ordpss  44450  19.41rg  44550  relpfrlem  44953  modelaxreplem2  44979  stoweidlem34  46043  ormklocald  46883  evenwodadd  46897  cfsetsnfsetf1  47068  fcoresf1  47078  euoreqb  47118  2reu8i  47122  ralralimp  47287  f1oresf1o2  47300  zm1nn  47311  elfz2z  47324  2tceilhalfelfzo1  47341  iccpartlt  47418  iccelpart  47427  icceuelpartlem  47429  fargshiftf1  47435  sprsymrelf1lem  47485  paireqne  47505  reuopreuprim  47520  goldbachthlem2  47540  odz2prm2pw  47557  fmtnoprmfac1lem  47558  fmtnofac2lem  47562  prmdvdsfmtnof1  47581  sfprmdvdsmersenne  47597  lighneallem2  47600  lighneallem4  47604  fppr2odd  47725  gbegt5  47755  gbowge7  47757  bgoldbtbndlem4  47802  bgoldbtbnd  47803  tgoldbach  47811  grimuhgr  47880  grimcnv  47881  grimco  47882  isuspgrim0  47887  isuspgrimlem  47888  upgrimwlklem5  47894  upgrimtrlslem2  47898  uhgrimisgrgriclem  47923  clnbgrgrimlem  47926  clnbgrgrim  47927  grimedg  47928  grtriprop  47933  isubgr3stgrlem3  47960  isubgr3stgrlem4  47961  isubgr3stgrlem6  47963  isubgr3stgrlem7  47964  uspgrlimlem3  47982  grlimgrtrilem2  47987  grlimgrtri  47988  grlicsym  47998  gpgedgvtx1  48046  lcosslsp  48394  lindslinindsimp1  48413  snlindsntor  48427  m1modmmod  48481  itcovalt2  48637  eenglngeehlnmlem2  48698  itsclc0yqsol  48724  itschlc0xyqsol1  48726  itschlc0xyqsol  48727  opnneilv  48863  i0oii  48874  io1ii  48875  iscnrm3lem4  48890  iscnrm3r  48902  setrec1lem4  49534  aacllem  49645