Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30488 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  180  sylibd  240  sylbid  241  sylibrd  260  sylbird  261  syland  609  animpimp2impd  852  ax12v2  2191  alrimdd  2226  axc16g  2272  axc16nf  2275  axc11r  2376  sb4a  2488  2eu1  2654  2eu1v  2655  ss2ralv  3985  ss2rexv  3986  trel3  5188  poss  5528  sess2  5584  wefrc  5612  wereu2  5615  predtrss  6273  frpomin  6291  funun  6531  ssimaex  6912  f1cofveqaeq  7201  f1imass  7208  soisoi  7272  isores3  7279  isofrlem  7284  isoselem  7285  weniso  7298  abnexg  7699  oninton  7738  orduniorsuc  7770  limuni3  7792  tfindsg  7801  limom  7822  resf1extb  7874  f1o2ndf1  8061  soxp  8069  xpord3inddlem  8094  soseq  8099  extmptsuppeq  8128  smoel  8290  tfrlem9  8314  tz7.49  8374  seqomlem1  8379  odi  8504  omass  8505  omeulem2  8508  oeordsuc  8520  oeeulem  8527  naddsuc2  8627  ertr  8649  swoord2  8667  ecopovtrn  8757  domtriord  9051  pssnn  9093  unxpdomlem2  9157  isinf  9165  f1finf1o  9173  findcard3  9183  frfi  9185  unblem3  9194  supssd  9366  infssd  9397  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  20615  zrtermoringc  20647  lmodfopnelem2  20889  lssssr  20944  rnglidlmcl  21209  gzrngunitlem  21407  znunit  21538  frgpcyg  21548  lsmcss  21667  obselocv  21703  obslbs  21705  mhpvarcl  22136  cply1mul  22282  gsummoncoe1  22294  cpmatacl  22699  cpmatinvcl  22700  cpmatmcllem  22701  m2cpminvid2lem  22737  mp2pm2mplem4  22792  pm2mp  22808  chfacfisf  22837  chfacfisfcpmat  22838  chfacfscmul0  22841  chfacfpmmul0  22845  cayhamlem4  22871  ordtrest2lem  23186  leordtval2  23195  lecldbas  23202  cncls  23257  cncnp  23263  cnpresti  23271  lmcnp  23287  cnt0  23329  isreg2  23360  cmpsublem  23382  cmpsub  23383  tgcmp  23384  bwth  23393  dfconn2  23402  1stcfb  23428  1stcelcls  23444  islly2  23467  dislly  23480  reftr  23497  comppfsc  23515  kgencn2  23540  txcnp  23603  txindis  23617  txcmplem1  23624  txlm  23631  xkohaus  23636  cnmptcom  23661  kqfvima  23713  isr0  23720  fgss2  23857  fbasrn  23867  filuni  23868  ufilmax  23890  isufil2  23891  cfinufil  23911  fmfnfmlem1  23937  fmfnfmlem2  23938  fmfnfmlem4  23940  fmfnfm  23941  fmco  23944  flimopn  23958  hausflim  23964  flimrest  23966  fclsopn  23997  flimfnfcls  24011  alexsubALTlem2  24031  alexsubALTlem3  24032  alexsubALT  24034  ptcmplem2  24036  cnextcn  24050  symgtgp  24089  qustgplem  24104  tsmsres  24127  tsmsxplem1  24136  isucn2  24261  imasdsf1olem  24356  bldisj  24381  blssps  24407  blss  24408  metcnp3  24523  ngptgp  24619  nrginvrcn  24675  nmoleub  24714  xrsmopn  24796  icccmplem3  24808  reconnlem2  24811  rectbntr0  24816  rescncf  24882  iocopnst  24925  iccpnfcnv  24929  lebnumii  24951  nmoleub2lem  25099  nmhmcn  25105  iscfil3  25258  iscau2  25262  iscau3  25263  iscau4  25264  iscmet3lem2  25277  caussi  25282  equivcfil  25284  equivcau  25285  ivthlem2  25437  ivthlem3  25438  ovoliunlem2  25488  ovoliunnul  25492  ioombl1lem4  25546  dyadmax  25583  dyadmbl  25585  volsup2  25590  itg2le  25724  itg2const2  25726  itg2seq  25727  itgsplitioo  25823  rolle  25975  c1lip1  25982  dvivthlem1  25993  lhop1  25999  dvcnvrelem1  26002  dvfsumrlim  26016  ply1divmo  26119  ig1peu  26158  plypf1  26195  coeaddlem  26232  dvply2g  26269  fta1  26292  quotcan  26293  aalioulem4  26319  ulmcaulem  26377  ulmcn  26382  pilem2  26435  sincosq1lem  26479  sinq12gt0  26489  sinq12ge0  26490  tanord1  26519  lognegb  26572  logrec  26745  logbgcd1irr  26776  dcubic  26828  xrlimcnp  26950  o1cxp  26956  ftalem2  27055  ftalem3  27056  fsumdvdscom  27166  chtub  27193  vmasum  27197  bcmono  27258  bposlem3  27267  bposlem7  27271  lgsdir  27313  lgsqrlem2  27328  lgsqrmodndvds  27334  gausslemma2dlem6  27353  gausslemma2d  27355  lgsquadlem2  27362  2lgslem3a1  27381  2lgslem3b1  27382  2lgslem3c1  27383  2lgslem3d1  27384  2sqlem6  27404  2sq2  27414  2sqmod  27417  dchrisumlem3  27472  pntrsumbnd2  27548  pntpbnd1  27567  pntibnd  27574  pntlem3  27590  pntleml  27592  ltsres  27644  nosepon  27647  nolesgn2o  27653  nogesgn1o  27655  nodenselem8  27673  nosupbnd1lem1  27690  madess  27876  madebdaylemlrcut  27909  peano5uzs  28414  bdayfinbndlem1  28477  z12bday  28495  brbtwn2  28992  colinearalg  28997  axcontlem10  29060  edgupgr  29221  edglnl  29230  usgruspgrb  29270  subupgr  29374  uhgrspan1  29390  usgredgsscusgredg  29546  fusgrn0degnn0  29586  upgrewlkle2  29693  uspgr2wlkeq  29732  redwlk  29757  wlkdlem2  29768  upgrwlkdvdelem  29822  pthdlem1  29852  pthdlem2  29854  crctcshwlkn0lem3  29898  wlkiswwlks1  29953  wwlksm1edg  29967  wwlksnred  29978  wwlksnextbi  29980  umgr2adedgspth  30034  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a  30086  clwlkclwwlkf1lem3  30094  clwwisshclwwslemlem  30101  clwwlkf  30135  clwwlkext2edg  30144  wwlksubclwwlk  30146  clwwlknonex2lem2  30196  eupth2lems  30326  frgrwopreglem4a  30398  frgrregorufrg  30414  ex-natded5.3-2  30496  isgrpo  30586  vacn  30783  ubthlem2  30960  htthlem  31006  normgt0  31216  shmodsi  31478  spansneleq  31659  h1datomi  31670  nmcexi  32115  pjnormssi  32257  stm1add3i  32336  golem2  32361  cvnsym  32379  dmdmd  32389  mdslmd1lem1  32414  mdslmd1i  32418  mdexchi  32424  atcveq0  32437  superpos  32443  hatomistici  32451  atoml2i  32472  atcvat2i  32476  chirredlem1  32479  atcvat3i  32485  mdsymlem3  32494  mdsymlem5  32496  cdj3lem2b  32526  cdj3i  32530  submarchi  33267  dfufd2  33633  tpr2rico  34096  ordtrest2NEWlem  34106  xrge0iifcnv  34117  omssubadd  34484  eulerpartlemb  34552  ballotlemfc0  34677  ballotlemfcc  34678  ftc2re  34782  fissorduni  35271  fineqvinfep  35306  axsepg2  35321  axsepg4  35324  axpowg2  35328  axpowg3  35329  loop1cycl  35365  subfacp1lem6  35413  iccllysconn  35478  cvmfolem  35507  satfsschain  35592  satfrel  35595  satfdm  35597  sat1el2xp  35607  satffunlem1lem1  35630  dmopab3rexdif  35633  satffunlem2lem2  35634  satffun  35637  fundmpss  35995  dfon2lem3  36011  dfon2lem6  36014  axextbdist  36026  dfrdg4  36179  5segofs  36234  cgrextend  36236  segconeu  36239  btwncomim  36241  btwnswapid  36245  btwnintr  36247  btwnexch3  36248  btwndiff  36255  ifscgr  36272  cgrxfr  36283  btwnxfr  36284  lineext  36304  brofs2  36305  linecgr  36309  lineid  36311  idinside  36312  endofsegid  36313  btwnconn1lem13  36327  btwnconn3  36331  finminlem  36546  nn0prpwlem  36550  cldbnd  36554  clsint2  36557  fnessref  36585  neibastop3  36590  fgmin  36598  onsuct0  36669  limsucncmpi  36673  tr0elw  36712  tr0el  36713  bj-nnfea  37077  bj-axc14  37209  bj-restn0  37448  bj-0int  37459  wl-19.2reqv  37895  wl-aetr  37900  wl-axc11r  37901  fin2so  37974  tan2h  37979  lindsenlbs  37982  poimirlem2  37989  poimirlem9  37996  poimirlem17  38004  poimirlem18  38005  poimirlem21  38008  poimirlem23  38010  poimirlem26  38013  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  poimir  38020  heicant  38022  mblfinlem2  38025  mblfinlem3  38026  itg2addnclem  38038  itg2addnclem2  38039  itg2gt0cn  38042  ftc1anclem5  38064  ftc1anclem6  38065  filbcmb  38107  nninfnub  38118  mettrifi  38124  geomcau  38126  istotbnd3  38138  sstotbnd2  38141  ismtybndlem  38173  heibor1lem  38176  heiborlem1  38178  heiborlem8  38185  heiborlem10  38187  heibor  38188  opidonOLD  38219  riscer  38355  crngohomfo  38373  keridl  38399  ispridl2  38405  ispridlc  38437  ac6s6  38539  eqvreltr  39058  eldisjdmqsim  39184  suceldisj  39185  eldisjs6  39307  dral1-o  39396  ax12indalem  39437  ax12inda2ALT  39438  lsatcveq0  39524  eqlkr3  39593  atlatmstc  39811  atlrelat1  39813  hlrelat2  39895  intnatN  39899  cvrexchlem  39911  cvratlem  39913  cvrat2  39921  atltcvr  39927  cvrat3  39934  cvrat4  39935  ps-1  39969  ps-2  39970  lplnnle2at  40033  lvolnle3at  40074  2llnma3r  40280  cdlemblem  40285  pmapjoin  40344  elpcliN  40385  lhpmcvr4N  40518  4atexlemnclw  40562  trlnidatb  40669  cdlemc4  40686  cdlemd3  40692  cdleme3g  40726  cdleme7d  40738  cdleme11c  40753  cdleme11dN  40754  cdleme21b  40818  cdleme21c  40819  cdleme21i  40827  cdleme22b  40833  cdleme35fnpq  40941  cdlemf1  41053  trlord  41061  cdlemg6c  41112  dihglblem6  41832  dochlkr  41877  dochkrshp  41878  dihjat1lem  41920  dochexmidlem5  41956  dochexmidlem8  41959  qsalrel  42725  remulcand  42916  prjspner1  43076  fphpdo  43262  pellexlem5  43278  pellexlem6  43279  jm2.26lem3  43446  unxpwdom3  43540  omlimcl2  43687  oe0suclim  43722  cantnfresb  43769  tfsconcatb0  43789  naddgeoa  43839  iscard5  43980  sqrtcval  44085  ov2ssiunov2  44144  frege124d  44205  ordpss  44894  19.41rg  44994  relpfrlem  45397  modelaxreplem2  45423  stoweidlem34  46477  ormklocald  47319  evenwodadd  47332  cfsetsnfsetf1  47522  fcoresf1  47532  euoreqb  47572  2reu8i  47576  ralralimp  47741  f1oresf1o2  47754  zm1nn  47765  elfz2z  47778  2tceilhalfelfzo1  47799  m1modmmod  47827  modlt0b  47832  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartlt  47899  iccelpart  47908  icceuelpartlem  47910  fargshiftf1  47916  sprsymrelf1lem  47966  paireqne  47986  reuopreuprim  48001  goldbachthlem2  48024  odz2prm2pw  48041  fmtnoprmfac1lem  48042  fmtnofac2lem  48046  prmdvdsfmtnof1  48065  sfprmdvdsmersenne  48081  lighneallem2  48084  lighneallem4  48088  fppr2odd  48222  gbegt5  48252  gbowge7  48254  bgoldbtbndlem4  48299  bgoldbtbnd  48300  tgoldbach  48308  grimuhgr  48378  grimcnv  48379  grimco  48380  isuspgrim0  48385  isuspgrimlem  48386  upgrimwlklem5  48392  upgrimtrlslem2  48396  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424  clnbgrgrim  48425  grimedg  48426  grtriprop  48432  isubgr3stgrlem3  48459  isubgr3stgrlem4  48460  isubgr3stgrlem6  48462  isubgr3stgrlem7  48463  uspgrlimlem3  48481  grlimedgclnbgr  48486  grlimgrtrilem2  48493  grlimgrtri  48494  grlicsym  48504  gpgedgvtx1  48553  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  lcosslsp  48929  lindslinindsimp1  48948  snlindsntor  48962  itcovalt2  49168  eenglngeehlnmlem2  49229  itsclc0yqsol  49255  itschlc0xyqsol1  49257  itschlc0xyqsol  49258  opnneilv  49399  i0oii  49410  io1ii  49411  iscnrm3lem4  49426  iscnrm3r  49438  setrec1lem4  50180  aacllem  50291