Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 30362 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  4008  ss2rexv  4009  trel3  5211  poss  5533  sess2  5589  wefrc  5617  wereu2  5620  predtrss  6274  frpomin  6292  funun  6532  ssimaex  6912  f1cofveqaeq  7198  f1imass  7205  soisoi  7269  isores3  7276  isofrlem  7281  isoselem  7282  weniso  7295  abnexg  7696  oninton  7735  orduniorsuc  7769  limuni3  7792  tfindsg  7801  limom  7822  resf1extb  7874  f1o2ndf1  8062  soxp  8069  xpord3inddlem  8094  soseq  8099  extmptsuppeq  8128  smoel  8290  tfrlem9  8314  tz7.49  8374  seqomlem1  8379  odi  8504  omass  8505  omeulem2  8508  oeordsuc  8519  oeeulem  8526  naddsuc2  8626  ertr  8647  swoord2  8665  ecopovtrn  8754  domtriord  9047  pssnn  9092  unxpdomlem2  9156  isinf  9165  isinfOLD  9166  f1finf1o  9174  findcard3  9187  findcard3OLD  9188  frfi  9190  unblem3  9199  supssd  9372  infssd  9403  en3lplem1  9527  inf3lem5  9547  cantnfle  9586  cantnfp1lem3  9595  ttrcltr  9631  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  10550  fpwwe2  10556  gchpwdom  10583  gchaclem  10591  tskr1om2  10681  inar1  10688  tskord  10693  tskuni  10696  grudomon  10730  grur1a  10732  grur1  10733  addnidpi  10814  ltexnq  10888  genpnnp  10918  addclprlem2  10930  mulclprlem  10932  psslinpr  10944  ltexprlem6  10954  ltexprlem7  10955  addcanpr  10959  mulgt0sr  11018  map2psrpr  11023  supsrlem  11024  axrrecex  11076  letr  11228  dedekind  11297  recex  11770  lemul12b  11999  mulgt1OLD  12001  fimaxre2  12088  lbreu  12093  nnrecgt0  12189  nnunb  12398  bndndx  12401  zeo  12580  uzind  12586  fzind  12592  fnn0ind  12593  suprfinzcl  12608  suprzcl2  12857  zmax  12864  rpnnen1lem5  12900  xrletr  13078  qbtwnre  13119  qsqueeze  13121  qextltlem  13122  xralrple  13125  xlesubadd  13183  supxrunb1  13239  icoshft  13394  zltaddlt1le  13426  fzen  13462  elfz0fzfz0  13554  elfzmlbp  13560  elfzo0z  13622  fzofzim  13630  fzo1fzo0n0  13636  elfzodifsumelfzo  13652  ssfzoulel  13681  modadd1  13830  modmul1  13849  uzrdgfni  13883  fsuppmapnn0fiub0  13918  fsuppmapnn0ub  13920  fsuppmapnn0fz  13921  seqf1olem1  13966  seqf1olem2  13967  expnbnd  14157  faclbnd4lem4  14221  hashgt23el  14349  seqcoll  14389  hashle2pr  14402  elss2prb  14413  ccatalpha  14518  swrdsbslen  14589  swrdspsleq  14590  swrdswrdlem  14628  swrdswrd  14629  pfxccatin12lem2a  14651  pfxccatin12lem1  14652  pfxccatin12lem3  14656  swrdccat3blem  14663  reuccatpfxs1lem  14670  repswswrd  14708  cshf1  14734  swrd2lsw  14877  sqeqd  15091  sqrmo  15176  cau3lem  15280  icodiamlt  15363  limsupbnd2  15408  lo1bdd2  15449  climuni  15477  rlimcn3  15515  mulcn2  15521  o1of2  15538  rlimo1  15542  lo1le  15577  iseralt  15610  cvgrat  15808  fprodss  15873  rpnnen2lem12  16152  ruclem3  16160  sqrt2irr  16176  p1modz1  16188  dvdsmodexp  16189  dvds2lem  16197  dvdslelem  16238  dvdsabseq  16242  divalglem8  16329  bitsinv1lem  16370  sadcaddlem  16386  smu01lem  16414  smueqlem  16419  bezoutlem4  16471  dfgcd2  16475  algcvga  16508  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  lcmfdvdsb  16572  coprmgcdb  16578  coprmdvds2  16583  coprmprod  16590  isprm3  16612  prmdvdsfz  16634  isprm5  16636  coprm  16640  rpexp12i  16653  phibndlem  16699  dfphi2  16703  eulerthlem2  16711  odzdvds  16725  iserodd  16765  pclem  16768  pcpremul  16773  pcqcl  16786  pcdvdsb  16799  pcprmpw2  16812  difsqpwdvds  16817  pcaddlem  16818  pcmptcl  16821  pcfac  16829  prmpwdvds  16834  unbenlem  16838  prmreclem1  16846  4sqlem17  16891  vdwmc2  16909  vdwlem9  16919  vdwlem10  16920  vdwlem13  16923  vdwnnlem3  16927  ramcl  16959  prmgaplem7  16987  mreiincl  17516  initoid  17926  termoid  17927  initoeu2lem1  17939  pospo  18267  resspos  18353  resstos  18354  dirge  18527  cyccom  19100  gsmsymgrfixlem1  19324  oddvdsnn0  19441  oddvds  19444  odcl2  19462  gexdvds  19481  sylow2alem2  19515  sylow2a  19516  efgi2  19622  efgsrel  19631  efgs1b  19633  imasabl  19773  cyggex2  19794  telgsums  19890  pgpfac1lem2  19974  pgpfac1lem3a  19975  pgpfac1lem3  19976  pgpfac1lem5  19978  zrtermorngc  20546  zrtermoringc  20578  lmodfopnelem2  20820  lssssr  20875  rnglidlmcl  21141  gzrngunitlem  21357  znunit  21488  frgpcyg  21498  lsmcss  21617  obselocv  21653  obslbs  21655  mhpvarcl  22051  cply1mul  22199  gsummoncoe1  22211  cpmatacl  22619  cpmatinvcl  22620  cpmatmcllem  22621  m2cpminvid2lem  22657  mp2pm2mplem4  22712  pm2mp  22728  chfacfisf  22757  chfacfisfcpmat  22758  chfacfscmul0  22761  chfacfpmmul0  22765  cayhamlem4  22791  ordtrest2lem  23106  leordtval2  23115  lecldbas  23122  cncls  23177  cncnp  23183  cnpresti  23191  lmcnp  23207  cnt0  23249  isreg2  23280  cmpsublem  23302  cmpsub  23303  tgcmp  23304  bwth  23313  dfconn2  23322  1stcfb  23348  1stcelcls  23364  islly2  23387  dislly  23400  reftr  23417  comppfsc  23435  kgencn2  23460  txcnp  23523  txindis  23537  txcmplem1  23544  txlm  23551  xkohaus  23556  cnmptcom  23581  kqfvima  23633  isr0  23640  fgss2  23777  fbasrn  23787  filuni  23788  ufilmax  23810  isufil2  23811  cfinufil  23831  fmfnfmlem1  23857  fmfnfmlem2  23858  fmfnfmlem4  23860  fmfnfm  23861  fmco  23864  flimopn  23878  hausflim  23884  flimrest  23886  fclsopn  23917  flimfnfcls  23931  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALT  23954  ptcmplem2  23956  cnextcn  23970  symgtgp  24009  qustgplem  24024  tsmsres  24047  tsmsxplem1  24056  isucn2  24182  imasdsf1olem  24277  bldisj  24302  blssps  24328  blss  24329  metcnp3  24444  ngptgp  24540  nrginvrcn  24596  nmoleub  24635  xrsmopn  24717  icccmplem3  24729  reconnlem2  24732  rectbntr0  24737  rescncf  24806  iocopnst  24853  iccpnfcnv  24858  lebnumii  24881  nmoleub2lem  25030  nmhmcn  25036  iscfil3  25189  iscau2  25193  iscau3  25194  iscau4  25195  iscmet3lem2  25208  caussi  25213  equivcfil  25215  equivcau  25216  ivthlem2  25369  ivthlem3  25370  ovoliunlem2  25420  ovoliunnul  25424  ioombl1lem4  25478  dyadmax  25515  dyadmbl  25517  volsup2  25522  itg2le  25656  itg2const2  25658  itg2seq  25659  itgsplitioo  25755  rolle  25910  c1lip1  25918  dvivthlem1  25929  lhop1  25935  dvcnvrelem1  25938  dvfsumrlim  25954  ply1divmo  26057  ig1peu  26096  plypf1  26133  coeaddlem  26170  dvply2g  26208  fta1  26232  quotcan  26233  aalioulem4  26259  ulmcaulem  26319  ulmcn  26324  pilem2  26378  sincosq1lem  26422  sinq12gt0  26432  sinq12ge0  26433  tanord1  26462  lognegb  26515  logrec  26689  logbgcd1irr  26720  dcubic  26772  xrlimcnp  26894  o1cxp  26901  ftalem2  27000  ftalem3  27001  fsumdvdscom  27111  chtub  27139  vmasum  27143  bcmono  27204  bposlem3  27213  bposlem7  27217  lgsdir  27259  lgsqrlem2  27274  lgsqrmodndvds  27280  gausslemma2dlem6  27299  gausslemma2d  27301  lgsquadlem2  27308  2lgslem3a1  27327  2lgslem3b1  27328  2lgslem3c1  27329  2lgslem3d1  27330  2sqlem6  27350  2sq2  27360  2sqmod  27363  dchrisumlem3  27418  pntrsumbnd2  27494  pntpbnd1  27513  pntibnd  27520  pntlem3  27536  pntleml  27538  sltres  27590  nosepon  27593  nolesgn2o  27599  nogesgn1o  27601  nodenselem8  27619  nosupbnd1lem1  27636  madess  27808  madebdaylemlrcut  27831  peano5uzs  28315  brbtwn2  28868  colinearalg  28873  axcontlem10  28936  edgupgr  29097  edglnl  29106  usgruspgrb  29146  subupgr  29250  uhgrspan1  29266  usgredgsscusgredg  29423  fusgrn0degnn0  29463  upgrewlkle2  29570  uspgr2wlkeq  29609  redwlk  29634  wlkdlem2  29645  upgrwlkdvdelem  29699  pthdlem1  29729  pthdlem2  29731  crctcshwlkn0lem3  29775  wlkiswwlks1  29830  wwlksm1edg  29844  wwlksnred  29855  wwlksnextbi  29857  umgr2adedgspth  29911  clwlkclwwlklem2fv2  29958  clwlkclwwlklem2a  29960  clwlkclwwlkf1lem3  29968  clwwisshclwwslemlem  29975  clwwlkf  30009  clwwlkext2edg  30018  wwlksubclwwlk  30020  clwwlknonex2lem2  30070  eupth2lems  30200  frgrwopreglem4a  30272  frgrregorufrg  30288  ex-natded5.3-2  30370  isgrpo  30459  vacn  30656  ubthlem2  30833  htthlem  30879  normgt0  31089  shmodsi  31351  spansneleq  31532  h1datomi  31543  nmcexi  31988  pjnormssi  32130  stm1add3i  32209  golem2  32234  cvnsym  32252  dmdmd  32262  mdslmd1lem1  32287  mdslmd1i  32291  mdexchi  32297  atcveq0  32310  superpos  32316  hatomistici  32324  atoml2i  32345  atcvat2i  32349  chirredlem1  32352  atcvat3i  32358  mdsymlem3  32367  mdsymlem5  32369  cdj3lem2b  32399  cdj3i  32403  submarchi  33141  dfufd2  33500  tpr2rico  33881  ordtrest2NEWlem  33891  xrge0iifcnv  33902  omssubadd  34270  eulerpartlemb  34338  ballotlemfc0  34463  ballotlemfcc  34464  ftc2re  34568  loop1cycl  35112  subfacp1lem6  35160  iccllysconn  35225  cvmfolem  35254  satfsschain  35339  satfrel  35342  satfdm  35344  sat1el2xp  35354  satffunlem1lem1  35377  dmopab3rexdif  35380  satffunlem2lem2  35381  satffun  35384  fundmpss  35742  dfon2lem3  35761  dfon2lem6  35764  axextbdist  35776  dfrdg4  35927  5segofs  35982  cgrextend  35984  segconeu  35987  btwncomim  35989  btwnswapid  35993  btwnintr  35995  btwnexch3  35996  btwndiff  36003  ifscgr  36020  cgrxfr  36031  btwnxfr  36032  lineext  36052  brofs2  36053  linecgr  36057  lineid  36059  idinside  36060  endofsegid  36061  btwnconn1lem13  36075  btwnconn3  36079  finminlem  36294  nn0prpwlem  36298  cldbnd  36302  clsint2  36305  fnessref  36333  neibastop3  36338  fgmin  36346  onsuct0  36417  limsucncmpi  36421  bj-nnfea  36710  bj-axc14  36832  bj-restn0  37066  bj-0int  37077  wl-19.2reqv  37500  wl-aetr  37505  wl-axc11r  37506  fin2so  37589  tan2h  37594  lindsenlbs  37597  poimirlem2  37604  poimirlem9  37611  poimirlem17  37619  poimirlem18  37620  poimirlem21  37623  poimirlem23  37625  poimirlem26  37628  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  poimir  37635  heicant  37637  mblfinlem2  37640  mblfinlem3  37641  itg2addnclem  37653  itg2addnclem2  37654  itg2gt0cn  37657  ftc1anclem5  37679  ftc1anclem6  37680  filbcmb  37722  nninfnub  37733  mettrifi  37739  geomcau  37741  istotbnd3  37753  sstotbnd2  37756  ismtybndlem  37788  heibor1lem  37791  heiborlem1  37793  heiborlem8  37800  heiborlem10  37802  heibor  37803  opidonOLD  37834  riscer  37970  crngohomfo  37988  keridl  38014  ispridl2  38020  ispridlc  38052  ac6s6  38154  eqvreltr  38586  dral1-o  38885  ax12indalem  38926  ax12inda2ALT  38927  lsatcveq0  39013  eqlkr3  39082  atlatmstc  39300  atlrelat1  39302  hlrelat2  39385  intnatN  39389  cvrexchlem  39401  cvratlem  39403  cvrat2  39411  atltcvr  39417  cvrat3  39424  cvrat4  39425  ps-1  39459  ps-2  39460  lplnnle2at  39523  lvolnle3at  39564  2llnma3r  39770  cdlemblem  39775  pmapjoin  39834  elpcliN  39875  lhpmcvr4N  40008  4atexlemnclw  40052  trlnidatb  40159  cdlemc4  40176  cdlemd3  40182  cdleme3g  40216  cdleme7d  40228  cdleme11c  40243  cdleme11dN  40244  cdleme21b  40308  cdleme21c  40309  cdleme21i  40317  cdleme22b  40323  cdleme35fnpq  40431  cdlemf1  40543  trlord  40551  cdlemg6c  40602  dihglblem6  41322  dochlkr  41367  dochkrshp  41368  dihjat1lem  41410  dochexmidlem5  41446  dochexmidlem8  41449  qsalrel  42216  remulcand  42415  prjspner1  42602  fphpdo  42793  pellexlem5  42809  pellexlem6  42810  jm2.26lem3  42977  unxpwdom3  43071  omlimcl2  43218  oe0suclim  43253  cantnfresb  43300  tfsconcatb0  43320  naddgeoa  43370  iscard5  43512  sqrtcval  43617  ov2ssiunov2  43676  frege124d  43737  ordpss  44427  19.41rg  44527  relpfrlem  44930  modelaxreplem2  44956  stoweidlem34  46019  ormklocald  46859  evenwodadd  46873  cfsetsnfsetf1  47047  fcoresf1  47057  euoreqb  47097  2reu8i  47101  ralralimp  47266  f1oresf1o2  47279  zm1nn  47290  elfz2z  47303  2tceilhalfelfzo1  47320  m1modmmod  47346  modlt0b  47351  iccpartlt  47412  iccelpart  47421  icceuelpartlem  47423  fargshiftf1  47429  sprsymrelf1lem  47479  paireqne  47499  reuopreuprim  47514  goldbachthlem2  47534  odz2prm2pw  47551  fmtnoprmfac1lem  47552  fmtnofac2lem  47556  prmdvdsfmtnof1  47575  sfprmdvdsmersenne  47591  lighneallem2  47594  lighneallem4  47598  fppr2odd  47719  gbegt5  47749  gbowge7  47751  bgoldbtbndlem4  47796  bgoldbtbnd  47797  tgoldbach  47805  grimuhgr  47875  grimcnv  47876  grimco  47877  isuspgrim0  47882  isuspgrimlem  47883  upgrimwlklem5  47889  upgrimtrlslem2  47893  uhgrimisgrgriclem  47918  clnbgrgrimlem  47921  clnbgrgrim  47922  grimedg  47923  grtriprop  47929  isubgr3stgrlem3  47956  isubgr3stgrlem4  47957  isubgr3stgrlem6  47959  isubgr3stgrlem7  47960  uspgrlimlem3  47978  grlimedgclnbgr  47983  grlimgrtrilem2  47990  grlimgrtri  47991  grlicsym  48001  gpgedgvtx1  48050  gpgedgiov  48053  gpgedg2ov  48054  gpgedg2iv  48055  pgnioedg1  48096  pgnioedg2  48097  pgnioedg3  48098  pgnioedg4  48099  pgnioedg5  48100  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem5lem1  48108  pgnbgreunbgrlem5lem2  48109  pgnbgreunbgrlem5lem3  48110  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