Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30302 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  4014  ss2rexv  4015  trel3  5219  poss  5541  sess2  5597  wefrc  5625  wereu2  5628  predtrss  6283  frpomin  6301  funun  6546  ssimaex  6928  f1cofveqaeq  7214  f1imass  7221  soisoi  7285  isores3  7292  isofrlem  7297  isoselem  7298  weniso  7311  abnexg  7712  oninton  7751  orduniorsuc  7785  limuni3  7808  tfindsg  7817  limom  7838  resf1extb  7890  f1o2ndf1  8078  soxp  8085  xpord3inddlem  8110  soseq  8115  extmptsuppeq  8144  smoel  8306  tfrlem9  8330  tz7.49  8390  seqomlem1  8395  odi  8520  omass  8521  omeulem2  8524  oeordsuc  8535  oeeulem  8542  naddsuc2  8642  ertr  8663  swoord2  8681  ecopovtrn  8770  domtriord  9064  pssnn  9109  unxpdomlem2  9174  isinf  9183  isinfOLD  9184  f1finf1o  9192  findcard3  9205  findcard3OLD  9206  frfi  9208  unblem3  9217  supssd  9390  infssd  9421  en3lplem1  9541  inf3lem5  9561  cantnfle  9600  cantnfp1lem3  9609  ttrcltr  9645  frmin  9678  rankxpsuc  9811  tcrank  9813  ficardom  9890  carduni  9910  infxpenlem  9942  dfac8alem  9958  ac10ct  9963  ween  9964  alephdom  10010  alephle  10017  iscard3  10022  alephfp  10037  pwsdompw  10132  infdif  10137  cfslbn  10196  cofsmo  10198  cfcof  10203  fin1a2s  10343  domtriomlem  10371  ac6num  10408  zorn2lem3  10427  axdclem2  10449  imadomg  10463  iundom2g  10469  ficard  10494  fpwwe2lem7  10566  fpwwe2  10572  gchpwdom  10599  gchaclem  10607  tskr1om2  10697  inar1  10704  tskord  10709  tskuni  10712  grudomon  10746  grur1a  10748  grur1  10749  addnidpi  10830  ltexnq  10904  genpnnp  10934  addclprlem2  10946  mulclprlem  10948  psslinpr  10960  ltexprlem6  10970  ltexprlem7  10971  addcanpr  10975  mulgt0sr  11034  map2psrpr  11039  supsrlem  11040  axrrecex  11092  letr  11244  dedekind  11313  recex  11786  lemul12b  12015  mulgt1OLD  12017  fimaxre2  12104  lbreu  12109  nnrecgt0  12205  nnunb  12414  bndndx  12417  zeo  12596  uzind  12602  fzind  12608  fnn0ind  12609  suprfinzcl  12624  suprzcl2  12873  zmax  12880  rpnnen1lem5  12916  xrletr  13094  qbtwnre  13135  qsqueeze  13137  qextltlem  13138  xralrple  13141  xlesubadd  13199  supxrunb1  13255  icoshft  13410  zltaddlt1le  13442  fzen  13478  elfz0fzfz0  13570  elfzmlbp  13576  elfzo0z  13638  fzofzim  13646  fzo1fzo0n0  13652  elfzodifsumelfzo  13668  ssfzoulel  13697  modadd1  13846  modmul1  13865  uzrdgfni  13899  fsuppmapnn0fiub0  13934  fsuppmapnn0ub  13936  fsuppmapnn0fz  13937  seqf1olem1  13982  seqf1olem2  13983  expnbnd  14173  faclbnd4lem4  14237  hashgt23el  14365  seqcoll  14405  hashle2pr  14418  elss2prb  14429  ccatalpha  14534  swrdsbslen  14605  swrdspsleq  14606  swrdswrdlem  14645  swrdswrd  14646  pfxccatin12lem2a  14668  pfxccatin12lem1  14669  pfxccatin12lem3  14673  swrdccat3blem  14680  reuccatpfxs1lem  14687  repswswrd  14725  cshf1  14751  swrd2lsw  14894  sqeqd  15108  sqrmo  15193  cau3lem  15297  icodiamlt  15380  limsupbnd2  15425  lo1bdd2  15466  climuni  15494  rlimcn3  15532  mulcn2  15538  o1of2  15555  rlimo1  15559  lo1le  15594  iseralt  15627  cvgrat  15825  fprodss  15890  rpnnen2lem12  16169  ruclem3  16177  sqrt2irr  16193  p1modz1  16205  dvdsmodexp  16206  dvds2lem  16214  dvdslelem  16255  dvdsabseq  16259  divalglem8  16346  bitsinv1lem  16387  sadcaddlem  16403  smu01lem  16431  smueqlem  16436  bezoutlem4  16488  dfgcd2  16492  algcvga  16525  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfdvdsb  16589  coprmgcdb  16595  coprmdvds2  16600  coprmprod  16607  isprm3  16629  prmdvdsfz  16651  isprm5  16653  coprm  16657  rpexp12i  16670  phibndlem  16716  dfphi2  16720  eulerthlem2  16728  odzdvds  16742  iserodd  16782  pclem  16785  pcpremul  16790  pcqcl  16803  pcdvdsb  16816  pcprmpw2  16829  difsqpwdvds  16834  pcaddlem  16835  pcmptcl  16838  pcfac  16846  prmpwdvds  16851  unbenlem  16855  prmreclem1  16863  4sqlem17  16908  vdwmc2  16926  vdwlem9  16936  vdwlem10  16937  vdwlem13  16940  vdwnnlem3  16944  ramcl  16976  prmgaplem7  17004  mreiincl  17533  initoid  17939  termoid  17940  initoeu2lem1  17952  pospo  18280  dirge  18538  cyccom  19111  gsmsymgrfixlem1  19333  oddvdsnn0  19450  oddvds  19453  odcl2  19471  gexdvds  19490  sylow2alem2  19524  sylow2a  19525  efgi2  19631  efgsrel  19640  efgs1b  19642  imasabl  19782  cyggex2  19803  telgsums  19899  pgpfac1lem2  19983  pgpfac1lem3a  19984  pgpfac1lem3  19985  pgpfac1lem5  19987  zrtermorngc  20528  zrtermoringc  20560  lmodfopnelem2  20781  lssssr  20836  rnglidlmcl  21102  gzrngunitlem  21325  znunit  21449  frgpcyg  21459  lsmcss  21577  obselocv  21613  obslbs  21615  mhpvarcl  22011  cply1mul  22159  gsummoncoe1  22171  cpmatacl  22579  cpmatinvcl  22580  cpmatmcllem  22581  m2cpminvid2lem  22617  mp2pm2mplem4  22672  pm2mp  22688  chfacfisf  22717  chfacfisfcpmat  22718  chfacfscmul0  22721  chfacfpmmul0  22725  cayhamlem4  22751  ordtrest2lem  23066  leordtval2  23075  lecldbas  23082  cncls  23137  cncnp  23143  cnpresti  23151  lmcnp  23167  cnt0  23209  isreg2  23240  cmpsublem  23262  cmpsub  23263  tgcmp  23264  bwth  23273  dfconn2  23282  1stcfb  23308  1stcelcls  23324  islly2  23347  dislly  23360  reftr  23377  comppfsc  23395  kgencn2  23420  txcnp  23483  txindis  23497  txcmplem1  23504  txlm  23511  xkohaus  23516  cnmptcom  23541  kqfvima  23593  isr0  23600  fgss2  23737  fbasrn  23747  filuni  23748  ufilmax  23770  isufil2  23771  cfinufil  23791  fmfnfmlem1  23817  fmfnfmlem2  23818  fmfnfmlem4  23820  fmfnfm  23821  fmco  23824  flimopn  23838  hausflim  23844  flimrest  23846  fclsopn  23877  flimfnfcls  23891  alexsubALTlem2  23911  alexsubALTlem3  23912  alexsubALT  23914  ptcmplem2  23916  cnextcn  23930  symgtgp  23969  qustgplem  23984  tsmsres  24007  tsmsxplem1  24016  isucn2  24142  imasdsf1olem  24237  bldisj  24262  blssps  24288  blss  24289  metcnp3  24404  ngptgp  24500  nrginvrcn  24556  nmoleub  24595  xrsmopn  24677  icccmplem3  24689  reconnlem2  24692  rectbntr0  24697  rescncf  24766  iocopnst  24813  iccpnfcnv  24818  lebnumii  24841  nmoleub2lem  24990  nmhmcn  24996  iscfil3  25149  iscau2  25153  iscau3  25154  iscau4  25155  iscmet3lem2  25168  caussi  25173  equivcfil  25175  equivcau  25176  ivthlem2  25329  ivthlem3  25330  ovoliunlem2  25380  ovoliunnul  25384  ioombl1lem4  25438  dyadmax  25475  dyadmbl  25477  volsup2  25482  itg2le  25616  itg2const2  25618  itg2seq  25619  itgsplitioo  25715  rolle  25870  c1lip1  25878  dvivthlem1  25889  lhop1  25895  dvcnvrelem1  25898  dvfsumrlim  25914  ply1divmo  26017  ig1peu  26056  plypf1  26093  coeaddlem  26130  dvply2g  26168  fta1  26192  quotcan  26193  aalioulem4  26219  ulmcaulem  26279  ulmcn  26284  pilem2  26338  sincosq1lem  26382  sinq12gt0  26392  sinq12ge0  26393  tanord1  26422  lognegb  26475  logrec  26649  logbgcd1irr  26680  dcubic  26732  xrlimcnp  26854  o1cxp  26861  ftalem2  26960  ftalem3  26961  fsumdvdscom  27071  chtub  27099  vmasum  27103  bcmono  27164  bposlem3  27173  bposlem7  27177  lgsdir  27219  lgsqrlem2  27234  lgsqrmodndvds  27240  gausslemma2dlem6  27259  gausslemma2d  27261  lgsquadlem2  27268  2lgslem3a1  27287  2lgslem3b1  27288  2lgslem3c1  27289  2lgslem3d1  27290  2sqlem6  27310  2sq2  27320  2sqmod  27323  dchrisumlem3  27378  pntrsumbnd2  27454  pntpbnd1  27473  pntibnd  27480  pntlem3  27496  pntleml  27498  sltres  27550  nosepon  27553  nolesgn2o  27559  nogesgn1o  27561  nodenselem8  27579  nosupbnd1lem1  27596  madess  27764  madebdaylemlrcut  27786  peano5uzs  28268  brbtwn2  28808  colinearalg  28813  axcontlem10  28876  edgupgr  29037  edglnl  29046  usgruspgrb  29086  subupgr  29190  uhgrspan1  29206  usgredgsscusgredg  29363  fusgrn0degnn0  29403  upgrewlkle2  29510  uspgr2wlkeq  29549  redwlk  29574  wlkdlem2  29585  upgrwlkdvdelem  29639  pthdlem1  29669  pthdlem2  29671  crctcshwlkn0lem3  29715  wlkiswwlks1  29770  wwlksm1edg  29784  wwlksnred  29795  wwlksnextbi  29797  umgr2adedgspth  29851  clwlkclwwlklem2fv2  29898  clwlkclwwlklem2a  29900  clwlkclwwlkf1lem3  29908  clwwisshclwwslemlem  29915  clwwlkf  29949  clwwlkext2edg  29958  wwlksubclwwlk  29960  clwwlknonex2lem2  30010  eupth2lems  30140  frgrwopreglem4a  30212  frgrregorufrg  30228  ex-natded5.3-2  30310  isgrpo  30399  vacn  30596  ubthlem2  30773  htthlem  30819  normgt0  31029  shmodsi  31291  spansneleq  31472  h1datomi  31483  nmcexi  31928  pjnormssi  32070  stm1add3i  32149  golem2  32174  cvnsym  32192  dmdmd  32202  mdslmd1lem1  32227  mdslmd1i  32231  mdexchi  32237  atcveq0  32250  superpos  32256  hatomistici  32264  atoml2i  32285  atcvat2i  32289  chirredlem1  32292  atcvat3i  32298  mdsymlem3  32307  mdsymlem5  32309  cdj3lem2b  32339  cdj3i  32343  resspos  32865  resstos  32866  submarchi  33113  dfufd2  33494  tpr2rico  33875  ordtrest2NEWlem  33885  xrge0iifcnv  33896  omssubadd  34264  eulerpartlemb  34332  ballotlemfc0  34457  ballotlemfcc  34458  ftc2re  34562  loop1cycl  35097  subfacp1lem6  35145  iccllysconn  35210  cvmfolem  35239  satfsschain  35324  satfrel  35327  satfdm  35329  sat1el2xp  35339  satffunlem1lem1  35362  dmopab3rexdif  35365  satffunlem2lem2  35366  satffun  35369  fundmpss  35727  dfon2lem3  35746  dfon2lem6  35749  axextbdist  35761  dfrdg4  35912  5segofs  35967  cgrextend  35969  segconeu  35972  btwncomim  35974  btwnswapid  35978  btwnintr  35980  btwnexch3  35981  btwndiff  35988  ifscgr  36005  cgrxfr  36016  btwnxfr  36017  lineext  36037  brofs2  36038  linecgr  36042  lineid  36044  idinside  36045  endofsegid  36046  btwnconn1lem13  36060  btwnconn3  36064  finminlem  36279  nn0prpwlem  36283  cldbnd  36287  clsint2  36290  fnessref  36318  neibastop3  36323  fgmin  36331  onsuct0  36402  limsucncmpi  36406  bj-nnfea  36695  bj-axc14  36817  bj-restn0  37051  bj-0int  37062  wl-19.2reqv  37485  wl-aetr  37490  wl-axc11r  37491  fin2so  37574  tan2h  37579  lindsenlbs  37582  poimirlem2  37589  poimirlem9  37596  poimirlem17  37604  poimirlem18  37605  poimirlem21  37608  poimirlem23  37610  poimirlem26  37613  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  poimir  37620  heicant  37622  mblfinlem2  37625  mblfinlem3  37626  itg2addnclem  37638  itg2addnclem2  37639  itg2gt0cn  37642  ftc1anclem5  37664  ftc1anclem6  37665  filbcmb  37707  nninfnub  37718  mettrifi  37724  geomcau  37726  istotbnd3  37738  sstotbnd2  37741  ismtybndlem  37773  heibor1lem  37776  heiborlem1  37778  heiborlem8  37785  heiborlem10  37787  heibor  37788  opidonOLD  37819  riscer  37955  crngohomfo  37973  keridl  37999  ispridl2  38005  ispridlc  38037  ac6s6  38139  eqvreltr  38571  dral1-o  38870  ax12indalem  38911  ax12inda2ALT  38912  lsatcveq0  38998  eqlkr3  39067  atlatmstc  39285  atlrelat1  39287  hlrelat2  39370  intnatN  39374  cvrexchlem  39386  cvratlem  39388  cvrat2  39396  atltcvr  39402  cvrat3  39409  cvrat4  39410  ps-1  39444  ps-2  39445  lplnnle2at  39508  lvolnle3at  39549  2llnma3r  39755  cdlemblem  39760  pmapjoin  39819  elpcliN  39860  lhpmcvr4N  39993  4atexlemnclw  40037  trlnidatb  40144  cdlemc4  40161  cdlemd3  40167  cdleme3g  40201  cdleme7d  40213  cdleme11c  40228  cdleme11dN  40229  cdleme21b  40293  cdleme21c  40294  cdleme21i  40302  cdleme22b  40308  cdleme35fnpq  40416  cdlemf1  40528  trlord  40536  cdlemg6c  40587  dihglblem6  41307  dochlkr  41352  dochkrshp  41353  dihjat1lem  41395  dochexmidlem5  41431  dochexmidlem8  41434  qsalrel  42201  remulcand  42400  prjspner1  42587  fphpdo  42778  pellexlem5  42794  pellexlem6  42795  jm2.26lem3  42963  unxpwdom3  43057  omlimcl2  43204  oe0suclim  43239  cantnfresb  43286  tfsconcatb0  43306  naddgeoa  43356  iscard5  43498  sqrtcval  43603  ov2ssiunov2  43662  frege124d  43723  ordpss  44413  19.41rg  44513  relpfrlem  44916  modelaxreplem2  44942  stoweidlem34  46005  ormklocald  46845  evenwodadd  46859  cfsetsnfsetf1  47033  fcoresf1  47043  euoreqb  47083  2reu8i  47087  ralralimp  47252  f1oresf1o2  47265  zm1nn  47276  elfz2z  47289  2tceilhalfelfzo1  47306  m1modmmod  47332  modlt0b  47337  iccpartlt  47398  iccelpart  47407  icceuelpartlem  47409  fargshiftf1  47415  sprsymrelf1lem  47465  paireqne  47485  reuopreuprim  47500  goldbachthlem2  47520  odz2prm2pw  47537  fmtnoprmfac1lem  47538  fmtnofac2lem  47542  prmdvdsfmtnof1  47561  sfprmdvdsmersenne  47577  lighneallem2  47580  lighneallem4  47584  fppr2odd  47705  gbegt5  47735  gbowge7  47737  bgoldbtbndlem4  47782  bgoldbtbnd  47783  tgoldbach  47791  grimuhgr  47860  grimcnv  47861  grimco  47862  isuspgrim0  47867  isuspgrimlem  47868  upgrimwlklem5  47874  upgrimtrlslem2  47878  uhgrimisgrgriclem  47903  clnbgrgrimlem  47906  clnbgrgrim  47907  grimedg  47908  grtriprop  47913  isubgr3stgrlem3  47940  isubgr3stgrlem4  47941  isubgr3stgrlem6  47943  isubgr3stgrlem7  47944  uspgrlimlem3  47962  grlimgrtrilem2  47967  grlimgrtri  47968  grlicsym  47978  gpgedgvtx1  48026  gpgedgiov  48029  gpgedg2ov  48030  gpgedg2iv  48031  pgnioedg1  48071  pgnioedg2  48072  pgnioedg3  48073  pgnioedg4  48074  pgnioedg5  48075  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5lem3  48085  lcosslsp  48400  lindslinindsimp1  48419  snlindsntor  48433  itcovalt2  48639  eenglngeehlnmlem2  48700  itsclc0yqsol  48726  itschlc0xyqsol1  48728  itschlc0xyqsol  48729  opnneilv  48870  i0oii  48881  io1ii  48882  iscnrm3lem4  48897  iscnrm3r  48909  setrec1lem4  49652  aacllem  49763