Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30470 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  2372  sb4a  2484  2eu1  2651  2eu1v  2652  ss2ralv  3992  ss2rexv  3993  trel3  5201  poss  5541  sess2  5597  wefrc  5625  wereu2  5628  predtrss  6286  frpomin  6304  funun  6544  ssimaex  6925  f1cofveqaeq  7212  f1imass  7219  soisoi  7283  isores3  7290  isofrlem  7295  isoselem  7296  weniso  7309  abnexg  7710  oninton  7749  orduniorsuc  7781  limuni3  7803  tfindsg  7812  limom  7833  resf1extb  7885  f1o2ndf1  8072  soxp  8079  xpord3inddlem  8104  soseq  8109  extmptsuppeq  8138  smoel  8300  tfrlem9  8324  tz7.49  8384  seqomlem1  8389  odi  8514  omass  8515  omeulem2  8518  oeordsuc  8530  oeeulem  8537  naddsuc2  8637  ertr  8659  swoord2  8677  ecopovtrn  8767  domtriord  9061  pssnn  9103  unxpdomlem2  9167  isinf  9175  f1finf1o  9183  findcard3  9193  frfi  9195  unblem3  9204  supssd  9376  infssd  9407  en3lplem1  9533  inf3lem5  9553  cantnfle  9592  cantnfp1lem3  9601  ttrcltr  9637  frmin  9673  rankxpsuc  9806  tcrank  9808  ficardom  9885  carduni  9905  infxpenlem  9935  dfac8alem  9951  ac10ct  9956  ween  9957  alephdom  10003  alephle  10010  iscard3  10015  alephfp  10030  pwsdompw  10125  infdif  10130  cfslbn  10189  cofsmo  10191  cfcof  10196  fin1a2s  10336  domtriomlem  10364  ac6num  10401  zorn2lem3  10420  axdclem2  10442  imadomg  10456  iundom2g  10462  ficard  10487  fpwwe2lem7  10560  fpwwe2  10566  gchpwdom  10593  gchaclem  10601  tskr1om2  10691  inar1  10698  tskord  10703  tskuni  10706  grudomon  10740  grur1a  10742  grur1  10743  addnidpi  10824  ltexnq  10898  genpnnp  10928  addclprlem2  10940  mulclprlem  10942  psslinpr  10954  ltexprlem6  10964  ltexprlem7  10965  addcanpr  10969  mulgt0sr  11028  map2psrpr  11033  supsrlem  11034  axrrecex  11086  letr  11240  dedekind  11309  recex  11782  lemul12b  12012  mulgt1OLD  12014  fimaxre2  12101  lbreu  12106  nnrecgt0  12220  nnunb  12433  bndndx  12436  zeo  12615  uzind  12621  fzind  12627  fnn0ind  12628  suprfinzcl  12643  suprzcl2  12888  zmax  12895  rpnnen1lem5  12931  xrletr  13109  qbtwnre  13151  qsqueeze  13153  qextltlem  13154  xralrple  13157  xlesubadd  13215  supxrunb1  13271  icoshft  13426  zltaddlt1le  13458  fzen  13495  elfz0fzfz0  13587  elfzmlbp  13593  elfzo0z  13656  fzofzim  13664  fzo1fzo0n0  13670  elfzodifsumelfzo  13686  ssfzoulel  13715  modadd1  13867  modmul1  13886  uzrdgfni  13920  fsuppmapnn0fiub0  13955  fsuppmapnn0ub  13957  fsuppmapnn0fz  13958  seqf1olem1  14003  seqf1olem2  14004  expnbnd  14194  faclbnd4lem4  14258  hashgt23el  14386  seqcoll  14426  hashle2pr  14439  elss2prb  14450  ccatalpha  14556  swrdsbslen  14627  swrdspsleq  14628  swrdswrdlem  14666  swrdswrd  14667  pfxccatin12lem2a  14689  pfxccatin12lem1  14690  pfxccatin12lem3  14694  swrdccat3blem  14701  reuccatpfxs1lem  14708  repswswrd  14746  cshf1  14772  swrd2lsw  14914  sqeqd  15128  sqrmo  15213  cau3lem  15317  icodiamlt  15400  limsupbnd2  15445  lo1bdd2  15486  climuni  15514  rlimcn3  15552  mulcn2  15558  o1of2  15575  rlimo1  15579  lo1le  15614  iseralt  15647  cvgrat  15848  fprodss  15913  rpnnen2lem12  16192  ruclem3  16200  sqrt2irr  16216  p1modz1  16228  dvdsmodexp  16229  dvds2lem  16237  dvdslelem  16278  dvdsabseq  16282  divalglem8  16369  bitsinv1lem  16410  sadcaddlem  16426  smu01lem  16454  smueqlem  16459  bezoutlem4  16511  dfgcd2  16515  algcvga  16548  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfdvdsb  16612  coprmgcdb  16618  coprmdvds2  16623  coprmprod  16630  isprm3  16652  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  17558  initoid  17968  termoid  17969  initoeu2lem1  17981  pospo  18309  resspos  18395  resstos  18396  dirge  18569  cyccom  19178  gsmsymgrfixlem1  19402  oddvdsnn0  19519  oddvds  19522  odcl2  19540  gexdvds  19559  sylow2alem2  19593  sylow2a  19594  efgi2  19700  efgsrel  19709  efgs1b  19711  imasabl  19851  cyggex2  19872  telgsums  19968  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem5  20056  zrtermorngc  20620  zrtermoringc  20652  lmodfopnelem2  20894  lssssr  20949  rnglidlmcl  21214  gzrngunitlem  21412  znunit  21543  frgpcyg  21553  lsmcss  21672  obselocv  21708  obslbs  21710  mhpvarcl  22114  cply1mul  22261  gsummoncoe1  22273  cpmatacl  22681  cpmatinvcl  22682  cpmatmcllem  22683  m2cpminvid2lem  22719  mp2pm2mplem4  22774  pm2mp  22790  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmul0  22823  chfacfpmmul0  22827  cayhamlem4  22853  ordtrest2lem  23168  leordtval2  23177  lecldbas  23184  cncls  23239  cncnp  23245  cnpresti  23253  lmcnp  23269  cnt0  23311  isreg2  23342  cmpsublem  23364  cmpsub  23365  tgcmp  23366  bwth  23375  dfconn2  23384  1stcfb  23410  1stcelcls  23426  islly2  23449  dislly  23462  reftr  23479  comppfsc  23497  kgencn2  23522  txcnp  23585  txindis  23599  txcmplem1  23606  txlm  23613  xkohaus  23618  cnmptcom  23643  kqfvima  23695  isr0  23702  fgss2  23839  fbasrn  23849  filuni  23850  ufilmax  23872  isufil2  23873  cfinufil  23893  fmfnfmlem1  23919  fmfnfmlem2  23920  fmfnfmlem4  23922  fmfnfm  23923  fmco  23926  flimopn  23940  hausflim  23946  flimrest  23948  fclsopn  23979  flimfnfcls  23993  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALT  24016  ptcmplem2  24018  cnextcn  24032  symgtgp  24071  qustgplem  24086  tsmsres  24109  tsmsxplem1  24118  isucn2  24243  imasdsf1olem  24338  bldisj  24363  blssps  24389  blss  24390  metcnp3  24505  ngptgp  24601  nrginvrcn  24657  nmoleub  24696  xrsmopn  24778  icccmplem3  24790  reconnlem2  24793  rectbntr0  24798  rescncf  24864  iocopnst  24907  iccpnfcnv  24911  lebnumii  24933  nmoleub2lem  25081  nmhmcn  25087  iscfil3  25240  iscau2  25244  iscau3  25245  iscau4  25246  iscmet3lem2  25259  caussi  25264  equivcfil  25266  equivcau  25267  ivthlem2  25419  ivthlem3  25420  ovoliunlem2  25470  ovoliunnul  25474  ioombl1lem4  25528  dyadmax  25565  dyadmbl  25567  volsup2  25572  itg2le  25706  itg2const2  25708  itg2seq  25709  itgsplitioo  25805  rolle  25957  c1lip1  25964  dvivthlem1  25975  lhop1  25981  dvcnvrelem1  25984  dvfsumrlim  25998  ply1divmo  26101  ig1peu  26140  plypf1  26177  coeaddlem  26214  dvply2g  26251  fta1  26274  quotcan  26275  aalioulem4  26301  ulmcaulem  26359  ulmcn  26364  pilem2  26417  sincosq1lem  26461  sinq12gt0  26471  sinq12ge0  26472  tanord1  26501  lognegb  26554  logrec  26727  logbgcd1irr  26758  dcubic  26810  xrlimcnp  26932  o1cxp  26938  ftalem2  27037  ftalem3  27038  fsumdvdscom  27148  chtub  27175  vmasum  27179  bcmono  27240  bposlem3  27249  bposlem7  27253  lgsdir  27295  lgsqrlem2  27310  lgsqrmodndvds  27316  gausslemma2dlem6  27335  gausslemma2d  27337  lgsquadlem2  27344  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2sqlem6  27386  2sq2  27396  2sqmod  27399  dchrisumlem3  27454  pntrsumbnd2  27530  pntpbnd1  27549  pntibnd  27556  pntlem3  27572  pntleml  27574  ltsres  27626  nosepon  27629  nolesgn2o  27635  nogesgn1o  27637  nodenselem8  27655  nosupbnd1lem1  27672  madess  27858  madebdaylemlrcut  27891  peano5uzs  28396  bdayfinbndlem1  28459  z12bday  28477  brbtwn2  28974  colinearalg  28979  axcontlem10  29042  edgupgr  29203  edglnl  29212  usgruspgrb  29252  subupgr  29356  uhgrspan1  29372  usgredgsscusgredg  29528  fusgrn0degnn0  29568  upgrewlkle2  29675  uspgr2wlkeq  29714  redwlk  29739  wlkdlem2  29750  upgrwlkdvdelem  29804  pthdlem1  29834  pthdlem2  29836  crctcshwlkn0lem3  29880  wlkiswwlks1  29935  wwlksm1edg  29949  wwlksnred  29960  wwlksnextbi  29962  umgr2adedgspth  30016  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a  30068  clwlkclwwlkf1lem3  30076  clwwisshclwwslemlem  30083  clwwlkf  30117  clwwlkext2edg  30126  wwlksubclwwlk  30128  clwwlknonex2lem2  30178  eupth2lems  30308  frgrwopreglem4a  30380  frgrregorufrg  30396  ex-natded5.3-2  30478  isgrpo  30568  vacn  30765  ubthlem2  30942  htthlem  30988  normgt0  31198  shmodsi  31460  spansneleq  31641  h1datomi  31652  nmcexi  32097  pjnormssi  32239  stm1add3i  32318  golem2  32343  cvnsym  32361  dmdmd  32371  mdslmd1lem1  32396  mdslmd1i  32400  mdexchi  32406  atcveq0  32419  superpos  32425  hatomistici  32433  atoml2i  32454  atcvat2i  32458  chirredlem1  32461  atcvat3i  32467  mdsymlem3  32476  mdsymlem5  32478  cdj3lem2b  32508  cdj3i  32512  submarchi  33247  dfufd2  33610  tpr2rico  34056  ordtrest2NEWlem  34066  xrge0iifcnv  34077  omssubadd  34444  eulerpartlemb  34512  ballotlemfc0  34637  ballotlemfcc  34638  ftc2re  34742  fissorduni  35233  fineqvinfep  35269  loop1cycl  35319  subfacp1lem6  35367  iccllysconn  35432  cvmfolem  35461  satfsschain  35546  satfrel  35549  satfdm  35551  sat1el2xp  35561  satffunlem1lem1  35584  dmopab3rexdif  35587  satffunlem2lem2  35588  satffun  35591  fundmpss  35949  dfon2lem3  35965  dfon2lem6  35968  axextbdist  35980  dfrdg4  36133  5segofs  36188  cgrextend  36190  segconeu  36193  btwncomim  36195  btwnswapid  36199  btwnintr  36201  btwnexch3  36202  btwndiff  36209  ifscgr  36226  cgrxfr  36237  btwnxfr  36238  lineext  36258  brofs2  36259  linecgr  36263  lineid  36265  idinside  36266  endofsegid  36267  btwnconn1lem13  36281  btwnconn3  36285  finminlem  36500  nn0prpwlem  36504  cldbnd  36508  clsint2  36511  fnessref  36539  neibastop3  36544  fgmin  36552  onsuct0  36623  limsucncmpi  36627  tr0elw  36666  tr0el  36667  bj-nnfea  37031  bj-axc14  37163  bj-restn0  37402  bj-0int  37413  wl-19.2reqv  37849  wl-aetr  37854  wl-axc11r  37855  fin2so  37928  tan2h  37933  lindsenlbs  37936  poimirlem2  37943  poimirlem9  37950  poimirlem17  37958  poimirlem18  37959  poimirlem21  37962  poimirlem23  37964  poimirlem26  37967  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimir  37974  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  itg2addnclem  37992  itg2addnclem2  37993  itg2gt0cn  37996  ftc1anclem5  38018  ftc1anclem6  38019  filbcmb  38061  nninfnub  38072  mettrifi  38078  geomcau  38080  istotbnd3  38092  sstotbnd2  38095  ismtybndlem  38127  heibor1lem  38130  heiborlem1  38132  heiborlem8  38139  heiborlem10  38141  heibor  38142  opidonOLD  38173  riscer  38309  crngohomfo  38327  keridl  38353  ispridl2  38359  ispridlc  38391  ac6s6  38493  eqvreltr  39012  eldisjdmqsim  39138  suceldisj  39139  eldisjs6  39261  dral1-o  39350  ax12indalem  39391  ax12inda2ALT  39392  lsatcveq0  39478  eqlkr3  39547  atlatmstc  39765  atlrelat1  39767  hlrelat2  39849  intnatN  39853  cvrexchlem  39865  cvratlem  39867  cvrat2  39875  atltcvr  39881  cvrat3  39888  cvrat4  39889  ps-1  39923  ps-2  39924  lplnnle2at  39987  lvolnle3at  40028  2llnma3r  40234  cdlemblem  40239  pmapjoin  40298  elpcliN  40339  lhpmcvr4N  40472  4atexlemnclw  40516  trlnidatb  40623  cdlemc4  40640  cdlemd3  40646  cdleme3g  40680  cdleme7d  40692  cdleme11c  40707  cdleme11dN  40708  cdleme21b  40772  cdleme21c  40773  cdleme21i  40781  cdleme22b  40787  cdleme35fnpq  40895  cdlemf1  41007  trlord  41015  cdlemg6c  41066  dihglblem6  41786  dochlkr  41831  dochkrshp  41832  dihjat1lem  41874  dochexmidlem5  41910  dochexmidlem8  41913  qsalrel  42680  remulcand  42871  prjspner1  43059  fphpdo  43245  pellexlem5  43261  pellexlem6  43262  jm2.26lem3  43429  unxpwdom3  43523  omlimcl2  43670  oe0suclim  43705  cantnfresb  43752  tfsconcatb0  43772  naddgeoa  43822  iscard5  43963  sqrtcval  44068  ov2ssiunov2  44127  frege124d  44188  ordpss  44877  19.41rg  44977  relpfrlem  45380  modelaxreplem2  45406  stoweidlem34  46462  ormklocald  47304  evenwodadd  47317  cfsetsnfsetf1  47507  fcoresf1  47517  euoreqb  47557  2reu8i  47561  ralralimp  47726  f1oresf1o2  47739  zm1nn  47750  elfz2z  47763  2tceilhalfelfzo1  47784  m1modmmod  47812  modlt0b  47817  muldvdsfacgt  47834  muldvdsfacm1  47835  iccpartlt  47884  iccelpart  47893  icceuelpartlem  47895  fargshiftf1  47901  sprsymrelf1lem  47951  paireqne  47971  reuopreuprim  47986  goldbachthlem2  48009  odz2prm2pw  48026  fmtnoprmfac1lem  48027  fmtnofac2lem  48031  prmdvdsfmtnof1  48050  sfprmdvdsmersenne  48066  lighneallem2  48069  lighneallem4  48073  fppr2odd  48207  gbegt5  48237  gbowge7  48239  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgoldbach  48293  grimuhgr  48363  grimcnv  48364  grimco  48365  isuspgrim0  48370  isuspgrimlem  48371  upgrimwlklem5  48377  upgrimtrlslem2  48381  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409  clnbgrgrim  48410  grimedg  48411  grtriprop  48417  isubgr3stgrlem3  48444  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  uspgrlimlem3  48466  grlimedgclnbgr  48471  grlimgrtrilem2  48478  grlimgrtri  48479  grlicsym  48489  gpgedgvtx1  48538  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  lcosslsp  48914  lindslinindsimp1  48933  snlindsntor  48947  itcovalt2  49153  eenglngeehlnmlem2  49214  itsclc0yqsol  49240  itschlc0xyqsol1  49242  itschlc0xyqsol  49243  opnneilv  49384  i0oii  49395  io1ii  49396  iscnrm3lem4  49411  iscnrm3r  49423  setrec1lem4  50165  aacllem  50276