Theorem syld 48

Description: Syllogism deduction. Deduction associated with syl 18. See conventions 31010 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 26	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpdd 44	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldc  49  3syld  61  sylsyld  62  nsyld  157  pm2.61d  181  sylibd  242  sylbid  243  sylibrd  262  sylbird  263  syland  615  animpimp2impd  860  ax12v2  2214  alrimdd  2250  axc16g  2294  axc16nf  2297  axc11r  2397  sb4a  2509  2eu1  2675  2eu1v  2676  ss2ralv  3980  ss2rexv  3981  trel3  5220  poss  5561  sess2  5617  wefrc  5645  wereu2  5648  predtrss  6328  frpomin  6346  ordpss  6394  funun  6591  ssimaex  6975  f1cofveqaeq  7265  f1imass  7272  soisoi  7340  isores3  7347  isofrlem  7352  isoselem  7353  weniso  7368  abnexg  7774  oninton  7813  orduniorsuc  7845  limuni3  7867  tfindsg  7876  limom  7897  resf1extb  7950  f1o2ndf1  8139  soxp  8147  xpord3inddlem  8177  soseq  8182  extmptsuppeq  8212  smoel  8375  tfrlem9  8400  tz7.49  8462  seqomlem1  8467  odi  8594  omass  8595  omeulem2  8598  oeordsuc  8610  oeeulem  8617  naddsuc2  8718  ertr  8740  swoord2  8758  ecopovtrn  8848  domtriord  9149  pssnn  9191  unxpdomlem2  9255  isinf  9263  f1finf1o  9271  findcard3  9281  frfi  9283  fissorduni  9289  unblem3  9293  supssd  9462  infssd  9493  en3lplem1  9620  inf3lem5  9640  cantnfle  9679  cantnfp1lem3  9688  ttrcltr  9724  frmin  9760  rankxpsuc  9906  tcrank  9908  setrec1lem4  9978  ficardom  10049  carduni  10069  infxpenlem  10099  dfac8alem  10115  ac10ct  10120  ween  10121  alephdom  10167  alephle  10174  iscard3  10179  alephfp  10194  pwsdompw  10288  infdif  10293  cfslbn  10352  cofsmo  10354  cfcof  10359  fin1a2s  10499  domtriomlem  10527  ac6num  10564  zorn2lem3  10583  axdclem2  10605  imadomg  10620  iundom2g  10631  ficard  10656  fpwwe2lem7  10729  fpwwe2  10735  gchpwdom  10762  gchaclem  10770  tskhf  10860  inar1  10867  tskord  10872  tskuni  10875  grudomon  10909  grur1a  10911  grur1  10912  addnidpi  10993  ltexnq  11067  genpnnp  11097  addclprlem2  11109  mulclprlem  11111  psslinpr  11123  ltexprlem6  11133  ltexprlem7  11134  addcanpr  11138  mulgt0sr  11197  map2psrpr  11202  supsrlem  11203  axrrecex  11255  dedekind  11480  recex  11955  lemul12b  12181  fimaxre2  12269  lbreu  12274  nnrecgt0  12388  nnunb  12609  bndndx  12612  zeo  12792  uzind  12798  fzind  12804  fnn0ind  12805  suprfinzcl  12820  suprzcl2  13072  zmax  13079  rpnnen1lem5  13116  xrletr  13294  qbtwnre  13336  qsqueeze  13338  qextltlem  13339  xralrple  13342  xlesubadd  13400  supxrunb1  13456  icoshft  13611  zltaddlt1le  13643  fzen  13681  elfz0fzfz0  13774  elfzmlbp  13780  elfzo0z  13843  fzofzim  13851  fzo1fzo0n0  13857  elfzodifsumelfzo  13873  ssfzoulel  13902  modadd1  14055  modmul1  14074  uzrdgfni  14108  fsuppmapnn0fiub0  14143  fsuppmapnn0ub  14145  fsuppmapnn0fz  14146  seqf1olem1  14191  seqf1olem2  14192  expnbnd  14383  faclbnd4lem4  14447  hashgt23el  14576  seqcoll  14616  hashle2pr  14629  elss2prb  14640  ccatalpha  14747  swrdsbslen  14822  swrdspsleq  14823  swrdswrdlem  14861  swrdswrd  14862  pfxccatin12lem2a  14884  pfxccatin12lem1  14885  pfxccatin12lem3  14889  swrdccat3blem  14896  reuccatpfxs1lem  14903  repswswrd  14943  cshf1  14969  swrd2lsw  15114  sqeqd  15342  sqrmo  15427  cau3lem  15531  icodiamlt  15614  limsupbnd2  15659  lo1bdd2  15700  climuni  15728  rlimcn3  15766  mulcn2  15772  o1of2  15789  rlimo1  15793  lo1le  15828  iseralt  15861  cvgrat  16061  fprodss  16124  rpnnen2lem12  16402  ruclem3  16410  sqrt2irr  16426  p1modz1  16438  dvdsmodexp  16439  dvds2lem  16447  dvdslelem  16488  dvdsabseq  16492  divalglem8  16579  bitsinv1lem  16620  sadcaddlem  16636  smu01lem  16664  smueqlem  16669  bezoutlem4  16724  dfgcd2  16728  algcvga  16763  lcmfunsnlem1  16821  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  lcmfdvdsb  16827  coprmgcdb  16833  coprmdvds2  16838  coprmprod  16845  isprm3  16867  prmdvdsfz  16890  isprm5  16892  coprm  16896  rpexp12i  16909  phibndlem  16956  dfphi2  16960  eulerthlem2  16968  odzdvds  16982  iserodd  17022  pclem  17025  pcpremul  17030  pcqcl  17043  pcdvdsb  17056  pcprmpw2  17069  difsqpwdvds  17074  pcaddlem  17075  pcmptcl  17078  pcfac  17086  prmpwdvds  17091  unbenlem  17095  prmreclem1  17103  4sqlem17  17148  vdwmc2  17166  vdwlem9  17176  vdwlem10  17177  vdwlem13  17180  vdwnnlem3  17184  ramcl  17216  prmgaplem7  17244  mreiincl  17775  initoid  18185  termoid  18186  initoeu2lem1  18198  pospo  18526  resspos  18612  resstos  18613  dirge  18786  mgmidpfod  18866  cyccom  19427  gsmsymgrfixlem1  19650  oddvdsnn0  19767  oddvds  19770  odcl2  19788  gexdvds  19807  sylow2alem2  19841  sylow2a  19842  efgi2  19948  efgsrel  19957  efgs1b  19959  imasabl  20099  cyggex2  20120  telgsums  20216  pgpfac1lem2  20300  pgpfac1lem3a  20301  pgpfac1lem3  20302  pgpfac1lem5  20304  crngrhmfo  20735  zrtermorngc  20904  zrtermoringc  20936  lmodfopnelem2  21183  lssssr  21238  rnglidlmcl  21504  unichnlidl  21525  gzrngunitlem  21747  znunit  21878  frgpcyg  21888  lsmcss  22007  obselocv  22043  obslbs  22045  lindsenlbs  22166  mhpvarcl  22478  cply1mul  22623  gsummoncoe1  22635  cpmatacl  23043  cpmatinvcl  23044  cpmatmcllem  23045  m2cpminvid2lem  23081  mp2pm2mplem4  23136  pm2mp  23152  chfacfisf  23181  chfacfisfcpmat  23182  chfacfscmul0  23185  chfacfpmmul0  23189  cayhamlem4  23215  ordtrest2lem  23530  leordtval2  23539  lecldbas  23546  cncls  23601  cncnp  23607  cnpresti  23615  lmcnp  23631  cnt0  23673  isreg2  23704  cmpsublem  23726  cmpsub  23727  tgcmp  23728  bwth  23737  dfconn2  23746  1stcfb  23772  1stcelcls  23789  islly2  23812  dislly  23825  reftr  23842  comppfsc  23860  kgencn2  23885  txcnp  23948  txindis  23962  txcmplem1  23969  txlm  23976  xkohaus  23981  cnmptcom  24006  kqfvima  24058  isr0  24065  fgss2  24202  fbasrn  24212  filuni  24213  ufilmax  24235  isufil2  24236  cfinufil  24256  fmfnfmlem1  24282  fmfnfmlem2  24283  fmfnfmlem4  24285  fmfnfm  24286  fmco  24289  flimopn  24303  hausflim  24309  flimrest  24311  fclsopn  24342  flimfnfcls  24356  alexsubALTlem2  24376  alexsubALTlem3  24377  alexsubALT  24379  ptcmplem2  24381  cnextcn  24395  symgtgp  24434  qustgplem  24449  tsmsres  24472  tsmsxplem1  24481  isucn2  24606  imasdsf1olem  24701  bldisj  24726  blssps  24752  blss  24753  metcnp3  24868  ngptgp  24964  nrginvrcn  25020  nmoleub  25059  xrsmopn  25141  icccmplem3  25153  reconnlem2  25156  rectbntr0  25161  rescncf  25227  iocopnst  25270  iccpnfcnv  25274  lebnumii  25296  nmoleub2lem  25444  nmhmcn  25450  iscfil3  25603  iscau2  25607  iscau3  25608  iscau4  25609  iscmet3lem2  25622  caussi  25627  equivcfil  25629  equivcau  25630  ivthlem2  25782  ivthlem3  25783  ovoliunlem2  25833  ovoliunnul  25837  ioombl1lem4  25891  dyadmax  25928  dyadmbl  25930  volsup2  25935  itg2le  26069  itg2const2  26071  itg2seq  26072  itgsplitioo  26167  rolle  26319  c1lip1  26326  dvivthlem1  26337  lhop1  26343  dvcnvrelem1  26346  dvfsumrlim  26360  ply1divmo  26463  ig1peu  26502  plypf1  26540  coeaddlem  26577  dvply2g  26615  fta1  26638  quotcan  26641  aalioulem4  26671  ulmcaulem  26730  ulmcn  26735  pilem2  26788  sincosq1lem  26835  sinq12gt0  26845  sinq12ge0  26846  tanord1  26874  lognegb  26927  logrec  27100  logbgcd1irr  27131  dcubic  27183  xrlimcnp  27305  o1cxp  27311  ftalem2  27410  ftalem3  27411  fsumdvdscom  27521  chtub  27548  vmasum  27552  bcmono  27613  bposlem3  27622  bposlem7  27626  lgsdir  27668  lgsqrlem2  27683  lgsqrmodndvds  27689  gausslemma2dlem6  27708  gausslemma2d  27710  lgsquadlem2  27717  2lgslem3a1  27736  2lgslem3b1  27737  2lgslem3c1  27738  2lgslem3d1  27739  2sqlem6  27759  2sq2  27769  2sqmod  27772  dchrisumlem3  27827  pntrsumbnd2  27903  pntpbnd1  27922  pntibnd  27929  pntlem3  27945  pntleml  27947  fltoprm  28004  ltsres  28028  nosepon  28031  nolesgn2o  28037  nogesgn1o  28039  nodenselem8  28057  nosupbnd1lem1  28074  madess  28261  madebdaylemlrcut  28294  peano5uzs  28799  bdayfinbndlem1  28862  z12bday  28880  brbtwn2  29492  colinearalg  29497  axcontlem10  29560  edgupgr  29721  edglnl  29730  usgruspgrb  29773  subupgr  29877  uhgrspan1  29893  usgredgsscusgredg  30049  fusgrn0degnn0  30089  upgrewlkle2  30196  uspgr2wlkeq  30235  redwlk  30260  wlkdlem2  30271  upgrwlkdvdelem  30331  pthdlem1  30361  pthdlem2  30363  crctcshwlkn0lem3  30410  wlkiswwlks1  30465  wwlksm1edg  30479  wwlksnred  30490  wwlksnextbi  30492  umgr2adedgspth  30546  clwlkclwwlklem2fv2  30596  clwlkclwwlklem2a  30598  clwlkclwwlkf1lem3  30606  clwwisshclwwslemlem  30613  clwwlkf  30647  clwwlkext2edg  30656  wwlksubclwwlk  30658  clwwlknonex2lem2  30708  loop1cycl  30753  eupth2lems  30848  frgrwopreglem4a  30920  frgrregorufrg  30936  ex-natded5.3-2  31018  isgrpo  31108  vacn  31305  ubthlem2  31482  htthlem  31528  normgt0  31738  shmodsi  32000  spansneleq  32181  h1datomi  32192  nmcexi  32637  pjnormssi  32779  stm1add3i  32858  golem2  32883  cvnsym  32901  dmdmd  32911  mdslmd1lem1  32936  mdslmd1i  32940  mdexchi  32946  atcveq0  32959  superpos  32965  hatomistici  32973  atoml2i  32994  atcvat2i  32998  chirredlem1  33001  atcvat3i  33007  mdsymlem3  33016  mdsymlem5  33018  cdj3lem2b  33048  cdj3i  33052  submarchi  33797  dfufd2  34132  tpr2rico  34594  ordtrest2NEWlem  34604  xrge0iifcnv  34615  omssubadd  34982  eulerpartlemb  35050  ballotlemfc0  35175  ballotlemfcc  35176  ftc2re  35277  fineqvinfep  35853  axsepg2  35868  axsepg4  35871  axpowg2  35875  axpowg3  35876  j0ltaleph  35951  subfacp1lem6  36040  iccllysconn  36105  cvmfolem  36134  satfsschain  36219  satfrel  36222  satfdm  36224  sat1el2xp  36234  satffunlem1lem1  36257  dmopab3rexdif  36260  satffunlem2lem2  36261  satffun  36264  fundmpss  36628  dfon2lem3  36643  dfon2lem6  36646  axextbdist  36658  dfrdg4  36811  5segofs  36867  cgrextend  36869  segconeu  36872  btwncomim  36874  btwnswapid  36878  btwnintr  36880  btwnexch3  36881  btwndiff  36888  ifscgr  36905  cgrxfr  36916  btwnxfr  36917  lineext  36937  brofs2  36938  linecgr  36942  lineid  36944  idinside  36945  endofsegid  36946  btwnconn1lem13  36960  btwnconn3  36964  finminlem  37202  nn0prpwlem  37206  cldbnd  37210  clsint2  37213  fnessref  37241  neibastop3  37246  fgmin  37254  onsuct0  37325  limsucncmpi  37329  tr0elw  37368  tr0el  37369  bj-nnfea  37732  bj-axc14  37864  bj-restn0  38119  bj-0int  38130  wl-19.2reqv  38565  wl-aetr  38570  wl-axc11r  38571  fin2so  38639  tan2h  38644  poimirlem2  38649  poimirlem9  38656  poimirlem17  38664  poimirlem18  38665  poimirlem21  38668  poimirlem23  38670  poimirlem26  38673  poimirlem29  38676  poimirlem30  38677  poimirlem31  38678  poimir  38680  heicant  38682  mblfinlem2  38685  mblfinlem3  38686  itg2addnclem  38698  itg2addnclem2  38699  itg2gt0cn  38702  ftc1anclem5  38724  ftc1anclem6  38725  findcard4  38741  dfprop2  38755  filbcmb  38783  nninfnub  38794  mettrifi  38800  geomcau  38802  istotbnd3  38814  sstotbnd2  38817  ismtybndlem  38849  heibor1lem  38852  heiborlem1  38854  heiborlem8  38861  heiborlem10  38863  heibor  38864  opidonOLD  38895  riscer  39031  crngohomfo  39049  keridl  39075  ispridl2  39081  ispridlc  39113  ac6s6  39213  eqvreltr  39732  eldisjdmqsim  39858  suceldisj  39859  eldisjs6  39981  dral1-o  40070  ax12indalem  40111  ax12inda2ALT  40112  lsatcveq0  40198  eqlkr3  40267  atlatmstc  40485  atlrelat1  40487  hlrelat2  40569  intnatN  40573  cvrexchlem  40585  cvratlem  40587  cvrat2  40595  atltcvr  40601  cvrat3  40608  cvrat4  40609  ps-1  40643  ps-2  40644  lplnnle2at  40707  lvolnle3at  40748  2llnma3r  40954  cdlemblem  40959  pmapjoin  41018  elpcliN  41059  lhpmcvr4N  41192  4atexlemnclw  41236  trlnidatb  41343  cdlemc4  41360  cdlemd3  41366  cdleme3g  41400  cdleme7d  41412  cdleme11c  41427  cdleme11dN  41428  cdleme21b  41492  cdleme21c  41493  cdleme21i  41501  cdleme22b  41507  cdleme35fnpq  41615  cdlemf1  41727  trlord  41735  cdlemg6c  41786  dihglblem6  42506  dochlkr  42551  dochkrshp  42552  dihjat1lem  42594  dochexmidlem5  42630  dochexmidlem8  42633  qsalrel  43401  remulcand  43599  fphpdo  43933  pellexlem5  43949  pellexlem6  43950  jm2.26lem3  44117  unxpwdom3  44206  omlimcl2  44353  oe0suclim  44388  cantnfresb  44435  tfsconcatb0  44455  naddgeoa  44505  iscard5  44646  sqrtcval  44750  ov2ssiunov2  44809  frege124d  44870  19.41rg  45641  relpfrlem  46051  modelaxreplem2  46077  stoweidlem34  47152  ormklocald  47994  evenwodadd  48019  cfsetsnfsetf1  48237  fcoresf1  48247  euoreqb  48288  2reu8i  48292  ralralimp  48456  f1oresf1o2  48469  zm1nn  48480  elfz2z  48493  2tceilhalfelfzo1  48514  m1modmmod  48542  modlt0b  48547  muldvdsfacgt  48564  muldvdsfacm1  48565  iccpartlt  48614  iccelpart  48623  icceuelpartlem  48625  fargshiftf1  48631  sprsymrelf1lem  48681  paireqne  48701  reuopreuprim  48716  goldbachthlem2  48739  odz2prm2pw  48756  fmtnoprmfac1lem  48757  fmtnofac2lem  48761  prmdvdsfmtnof1  48780  sfprmdvdsmersenne  48796  lighneallem2  48799  lighneallem4  48803  fppr2odd  48937  gbegt5  48967  gbowge7  48969  bgoldbtbndlem4  49014  bgoldbtbnd  49015  tgoldbach  49023  grimuhgr  49093  grimcnv  49094  grimco  49095  isuspgrim0  49100  isuspgrimlem  49101  upgrimwlklem5  49107  upgrimtrlslem2  49111  uhgrimisgrgriclem  49136  clnbgrgrimlem  49139  clnbgrgrim  49140  grimedg  49141  grtriprop  49147  isubgr3stgrlem3  49174  isubgr3stgrlem4  49175  isubgr3stgrlem6  49177  isubgr3stgrlem7  49178  uspgrlimlem3  49196  grlimedgclnbgr  49201  grlimgrtrilem2  49208  grlimgrtri  49209  grlicsym  49219  gpgedgvtx1  49268  gpgedgiov  49271  gpgedg2ov  49272  gpgedg2iv  49273  pgnioedg1  49314  pgnioedg2  49315  pgnioedg3  49316  pgnioedg4  49317  pgnioedg5  49318  pgnbgreunbgrlem2lem1  49320  pgnbgreunbgrlem2lem2  49321  pgnbgreunbgrlem2lem3  49322  pgnbgreunbgrlem5lem1  49326  pgnbgreunbgrlem5lem2  49327  pgnbgreunbgrlem5lem3  49328  lcosslsp  49658  lindslinindsimp1  49677  snlindsntor  49691  itcovalt2  49897  eenglngeehlnmlem2  49959  itsclc0yqsol  49984  itschlc0xyqsol1  49986  itschlc0xyqsol  49987  opnneilv  50131  i0oii  50142  io1ii  50143  iscnrm3lem4  50158  iscnrm3r  50170  aacllem  51122