Theorem syld 48

Description: Syllogism deduction. Deduction associated with syl 18. See conventions 30880 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  2215  alrimdd  2250  axc16g  2294  axc16nf  2297  axc11r  2397  sb4a  2509  2eu1  2675  2eu1v  2676  ss2ralv  4002  ss2rexv  4003  trel3  5221  poss  5565  sess2  5621  wefrc  5649  wereu2  5652  predtrss  6320  frpomin  6338  ordpss  6386  funun  6579  ssimaex  6963  f1cofveqaeq  7254  f1imass  7261  soisoi  7329  isores3  7336  isofrlem  7341  isoselem  7342  weniso  7357  abnexg  7755  oninton  7794  orduniorsuc  7826  limuni3  7848  tfindsg  7857  limom  7878  resf1extb  7931  f1o2ndf1  8119  soxp  8127  xpord3inddlem  8152  soseq  8157  extmptsuppeq  8186  smoel  8349  tfrlem9  8374  tz7.49  8434  seqomlem1  8439  odi  8566  omass  8567  omeulem2  8570  oeordsuc  8582  oeeulem  8589  naddsuc2  8690  ertr  8712  swoord2  8730  ecopovtrn  8820  domtriord  9121  pssnn  9163  unxpdomlem2  9227  isinf  9235  f1finf1o  9243  findcard3  9253  frfi  9255  unblem3  9264  supssd  9433  infssd  9464  en3lplem1  9591  inf3lem5  9611  cantnfle  9650  cantnfp1lem3  9659  ttrcltr  9695  frmin  9731  rankxpsuc  9864  tcrank  9866  ficardom  9966  carduni  9986  infxpenlem  10016  dfac8alem  10032  ac10ct  10037  ween  10038  alephdom  10084  alephle  10091  iscard3  10096  alephfp  10111  pwsdompw  10205  infdif  10210  cfslbn  10269  cofsmo  10271  cfcof  10276  fin1a2s  10416  domtriomlem  10444  ac6num  10481  zorn2lem3  10500  axdclem2  10522  imadomg  10537  iundom2g  10548  ficard  10573  fpwwe2lem7  10646  fpwwe2  10652  gchpwdom  10679  gchaclem  10687  tskr1om2  10777  inar1  10784  tskord  10789  tskuni  10792  grudomon  10826  grur1a  10828  grur1  10829  addnidpi  10910  ltexnq  10984  genpnnp  11014  addclprlem2  11026  mulclprlem  11028  psslinpr  11040  ltexprlem6  11050  ltexprlem7  11051  addcanpr  11055  mulgt0sr  11114  map2psrpr  11119  supsrlem  11120  axrrecex  11172  letr  11328  dedekind  11397  recex  11870  lemul12b  12096  fimaxre2  12184  lbreu  12189  nnrecgt0  12303  nnunb  12524  bndndx  12527  zeo  12707  uzind  12713  fzind  12719  fnn0ind  12720  suprfinzcl  12735  suprzcl2  12987  zmax  12994  rpnnen1lem5  13031  xrletr  13209  qbtwnre  13251  qsqueeze  13253  qextltlem  13254  xralrple  13257  xlesubadd  13315  supxrunb1  13371  icoshft  13526  zltaddlt1le  13558  fzen  13595  elfz0fzfz0  13688  elfzmlbp  13694  elfzo0z  13757  fzofzim  13765  fzo1fzo0n0  13771  elfzodifsumelfzo  13787  ssfzoulel  13816  modadd1  13969  modmul1  13988  uzrdgfni  14022  fsuppmapnn0fiub0  14057  fsuppmapnn0ub  14059  fsuppmapnn0fz  14060  seqf1olem1  14105  seqf1olem2  14106  expnbnd  14296  faclbnd4lem4  14360  hashgt23el  14489  seqcoll  14529  hashle2pr  14542  elss2prb  14553  ccatalpha  14660  swrdsbslen  14734  swrdspsleq  14735  swrdswrdlem  14773  swrdswrd  14774  pfxccatin12lem2a  14796  pfxccatin12lem1  14797  pfxccatin12lem3  14801  swrdccat3blem  14808  reuccatpfxs1lem  14815  repswswrd  14855  cshf1  14881  swrd2lsw  15025  sqeqd  15253  sqrmo  15338  cau3lem  15442  icodiamlt  15525  limsupbnd2  15570  lo1bdd2  15611  climuni  15639  rlimcn3  15677  mulcn2  15683  o1of2  15700  rlimo1  15704  lo1le  15739  iseralt  15772  cvgrat  15972  fprodss  16035  rpnnen2lem12  16313  ruclem3  16321  sqrt2irr  16337  p1modz1  16349  dvdsmodexp  16350  dvds2lem  16358  dvdslelem  16399  dvdsabseq  16403  divalglem8  16490  bitsinv1lem  16531  sadcaddlem  16547  smu01lem  16575  smueqlem  16580  bezoutlem4  16632  dfgcd2  16636  algcvga  16669  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  lcmfdvdsb  16733  coprmgcdb  16739  coprmdvds2  16744  coprmprod  16751  isprm3  16773  prmdvdsfz  16796  isprm5  16798  coprm  16802  rpexp12i  16815  phibndlem  16861  dfphi2  16865  eulerthlem2  16873  odzdvds  16887  iserodd  16927  pclem  16930  pcpremul  16935  pcqcl  16948  pcdvdsb  16961  pcprmpw2  16974  difsqpwdvds  16979  pcaddlem  16980  pcmptcl  16983  pcfac  16991  prmpwdvds  16996  unbenlem  17000  prmreclem1  17008  4sqlem17  17053  vdwmc2  17071  vdwlem9  17081  vdwlem10  17082  vdwlem13  17085  vdwnnlem3  17089  ramcl  17121  prmgaplem7  17149  mreiincl  17680  initoid  18090  termoid  18091  initoeu2lem1  18103  pospo  18431  resspos  18517  resstos  18518  dirge  18691  mgmidpfod  18770  cyccom  19331  gsmsymgrfixlem1  19554  oddvdsnn0  19671  oddvds  19674  odcl2  19692  gexdvds  19711  sylow2alem2  19745  sylow2a  19746  efgi2  19852  efgsrel  19861  efgs1b  19863  imasabl  20003  cyggex2  20024  telgsums  20120  pgpfac1lem2  20204  pgpfac1lem3a  20205  pgpfac1lem3  20206  pgpfac1lem5  20208  crngrhmfo  20637  zrtermorngc  20805  zrtermoringc  20837  lmodfopnelem2  21083  lssssr  21138  rnglidlmcl  21404  unichnlidl  21425  gzrngunitlem  21645  znunit  21776  frgpcyg  21786  lsmcss  21905  obselocv  21941  obslbs  21943  lindsenlbs  22064  mhpvarcl  22376  cply1mul  22521  gsummoncoe1  22533  cpmatacl  22941  cpmatinvcl  22942  cpmatmcllem  22943  m2cpminvid2lem  22979  mp2pm2mplem4  23034  pm2mp  23050  chfacfisf  23079  chfacfisfcpmat  23080  chfacfscmul0  23083  chfacfpmmul0  23087  cayhamlem4  23113  ordtrest2lem  23428  leordtval2  23437  lecldbas  23444  cncls  23499  cncnp  23505  cnpresti  23513  lmcnp  23529  cnt0  23571  isreg2  23602  cmpsublem  23624  cmpsub  23625  tgcmp  23626  bwth  23635  dfconn2  23644  1stcfb  23670  1stcelcls  23687  islly2  23710  dislly  23723  reftr  23740  comppfsc  23758  kgencn2  23783  txcnp  23846  txindis  23860  txcmplem1  23867  txlm  23874  xkohaus  23879  cnmptcom  23904  kqfvima  23956  isr0  23963  fgss2  24100  fbasrn  24110  filuni  24111  ufilmax  24133  isufil2  24134  cfinufil  24154  fmfnfmlem1  24180  fmfnfmlem2  24181  fmfnfmlem4  24183  fmfnfm  24184  fmco  24187  flimopn  24201  hausflim  24207  flimrest  24209  fclsopn  24240  flimfnfcls  24254  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALT  24277  ptcmplem2  24279  cnextcn  24293  symgtgp  24332  qustgplem  24347  tsmsres  24370  tsmsxplem1  24379  isucn2  24504  imasdsf1olem  24599  bldisj  24624  blssps  24650  blss  24651  metcnp3  24766  ngptgp  24862  nrginvrcn  24918  nmoleub  24957  xrsmopn  25039  icccmplem3  25051  reconnlem2  25054  rectbntr0  25059  rescncf  25125  iocopnst  25168  iccpnfcnv  25172  lebnumii  25194  nmoleub2lem  25342  nmhmcn  25348  iscfil3  25501  iscau2  25505  iscau3  25506  iscau4  25507  iscmet3lem2  25520  caussi  25525  equivcfil  25527  equivcau  25528  ivthlem2  25680  ivthlem3  25681  ovoliunlem2  25731  ovoliunnul  25735  ioombl1lem4  25789  dyadmax  25826  dyadmbl  25828  volsup2  25833  itg2le  25967  itg2const2  25969  itg2seq  25970  itgsplitioo  26065  rolle  26217  c1lip1  26224  dvivthlem1  26235  lhop1  26241  dvcnvrelem1  26244  dvfsumrlim  26258  ply1divmo  26361  ig1peu  26400  plypf1  26438  coeaddlem  26475  dvply2g  26515  fta1  26538  quotcan  26541  aalioulem4  26571  ulmcaulem  26630  ulmcn  26635  pilem2  26688  sincosq1lem  26735  sinq12gt0  26745  sinq12ge0  26746  tanord1  26774  lognegb  26827  logrec  27000  logbgcd1irr  27031  dcubic  27083  xrlimcnp  27205  o1cxp  27211  ftalem2  27310  ftalem3  27311  fsumdvdscom  27421  chtub  27448  vmasum  27452  bcmono  27513  bposlem3  27522  bposlem7  27526  lgsdir  27568  lgsqrlem2  27583  lgsqrmodndvds  27589  gausslemma2dlem6  27608  gausslemma2d  27610  lgsquadlem2  27617  2lgslem3a1  27636  2lgslem3b1  27637  2lgslem3c1  27638  2lgslem3d1  27639  2sqlem6  27659  2sq2  27669  2sqmod  27672  dchrisumlem3  27727  pntrsumbnd2  27803  pntpbnd1  27822  pntibnd  27829  pntlem3  27845  pntleml  27847  ltsres  27898  nosepon  27901  nolesgn2o  27907  nogesgn1o  27909  nodenselem8  27927  nosupbnd1lem1  27944  madess  28131  madebdaylemlrcut  28164  peano5uzs  28669  bdayfinbndlem1  28732  z12bday  28750  brbtwn2  29362  colinearalg  29367  axcontlem10  29430  edgupgr  29591  edglnl  29600  usgruspgrb  29643  subupgr  29747  uhgrspan1  29763  usgredgsscusgredg  29919  fusgrn0degnn0  29959  upgrewlkle2  30066  uspgr2wlkeq  30105  redwlk  30130  wlkdlem2  30141  upgrwlkdvdelem  30201  pthdlem1  30231  pthdlem2  30233  crctcshwlkn0lem3  30280  wlkiswwlks1  30335  wwlksm1edg  30349  wwlksnred  30360  wwlksnextbi  30362  umgr2adedgspth  30416  clwlkclwwlklem2fv2  30466  clwlkclwwlklem2a  30468  clwlkclwwlkf1lem3  30476  clwwisshclwwslemlem  30483  clwwlkf  30517  clwwlkext2edg  30526  wwlksubclwwlk  30528  clwwlknonex2lem2  30578  loop1cycl  30623  eupth2lems  30718  frgrwopreglem4a  30790  frgrregorufrg  30806  ex-natded5.3-2  30888  isgrpo  30978  vacn  31175  ubthlem2  31352  htthlem  31398  normgt0  31608  shmodsi  31870  spansneleq  32051  h1datomi  32062  nmcexi  32507  pjnormssi  32649  stm1add3i  32728  golem2  32753  cvnsym  32771  dmdmd  32781  mdslmd1lem1  32806  mdslmd1i  32810  mdexchi  32816  atcveq0  32829  superpos  32835  hatomistici  32843  atoml2i  32864  atcvat2i  32868  chirredlem1  32871  atcvat3i  32877  mdsymlem3  32886  mdsymlem5  32888  cdj3lem2b  32918  cdj3i  32922  submarchi  33626  dfufd2  33960  tpr2rico  34422  ordtrest2NEWlem  34432  xrge0iifcnv  34443  omssubadd  34811  eulerpartlemb  34879  ballotlemfc0  35004  ballotlemfcc  35005  ftc2re  35106  fissorduni  35594  fineqvinfep  35651  axsepg2  35666  axsepg4  35669  axpowg2  35673  axpowg3  35674  subfacp1lem6  35764  iccllysconn  35829  cvmfolem  35858  satfsschain  35943  satfrel  35946  satfdm  35948  sat1el2xp  35958  satffunlem1lem1  35981  dmopab3rexdif  35984  satffunlem2lem2  35985  satffun  35988  fundmpss  36346  dfon2lem3  36362  dfon2lem6  36365  axextbdist  36377  dfrdg4  36530  5segofs  36586  cgrextend  36588  segconeu  36591  btwncomim  36593  btwnswapid  36597  btwnintr  36599  btwnexch3  36600  btwndiff  36607  ifscgr  36624  cgrxfr  36635  btwnxfr  36636  lineext  36656  brofs2  36657  linecgr  36661  lineid  36663  idinside  36664  endofsegid  36665  btwnconn1lem13  36679  btwnconn3  36683  finminlem  36937  nn0prpwlem  36941  cldbnd  36945  clsint2  36948  fnessref  36976  neibastop3  36981  fgmin  36989  onsuct0  37060  limsucncmpi  37064  tr0elw  37103  tr0el  37104  bj-nnfea  37467  bj-axc14  37599  bj-restn0  37840  bj-0int  37851  wl-19.2reqv  38287  wl-aetr  38292  wl-axc11r  38293  fin2so  38361  tan2h  38366  poimirlem2  38371  poimirlem9  38378  poimirlem17  38386  poimirlem18  38387  poimirlem21  38390  poimirlem23  38392  poimirlem26  38395  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  poimir  38402  heicant  38404  mblfinlem2  38407  mblfinlem3  38408  itg2addnclem  38420  itg2addnclem2  38421  itg2gt0cn  38424  ftc1anclem5  38446  ftc1anclem6  38447  findcard4  38463  filbcmb  38490  nninfnub  38501  mettrifi  38507  geomcau  38509  istotbnd3  38521  sstotbnd2  38524  ismtybndlem  38556  heibor1lem  38559  heiborlem1  38561  heiborlem8  38568  heiborlem10  38570  heibor  38571  opidonOLD  38602  riscer  38738  crngohomfo  38756  keridl  38782  ispridl2  38788  ispridlc  38820  ac6s6  38920  eqvreltr  39439  eldisjdmqsim  39565  suceldisj  39566  eldisjs6  39688  dral1-o  39777  ax12indalem  39818  ax12inda2ALT  39819  lsatcveq0  39905  eqlkr3  39974  atlatmstc  40192  atlrelat1  40194  hlrelat2  40276  intnatN  40280  cvrexchlem  40292  cvratlem  40294  cvrat2  40302  atltcvr  40308  cvrat3  40315  cvrat4  40316  ps-1  40350  ps-2  40351  lplnnle2at  40414  lvolnle3at  40455  2llnma3r  40661  cdlemblem  40666  pmapjoin  40725  elpcliN  40766  lhpmcvr4N  40899  4atexlemnclw  40943  trlnidatb  41050  cdlemc4  41067  cdlemd3  41073  cdleme3g  41107  cdleme7d  41119  cdleme11c  41134  cdleme11dN  41135  cdleme21b  41199  cdleme21c  41200  cdleme21i  41208  cdleme22b  41214  cdleme35fnpq  41322  cdlemf1  41434  trlord  41442  cdlemg6c  41493  dihglblem6  42213  dochlkr  42258  dochkrshp  42259  dihjat1lem  42301  dochexmidlem5  42337  dochexmidlem8  42340  qsalrel  43108  remulcand  43314  prjspner1  43472  fphpdo  43658  pellexlem5  43674  pellexlem6  43675  jm2.26lem3  43842  unxpwdom3  43936  omlimcl2  44083  oe0suclim  44118  cantnfresb  44165  tfsconcatb0  44185  naddgeoa  44235  iscard5  44376  sqrtcval  44481  ov2ssiunov2  44540  frege124d  44601  19.41rg  45373  relpfrlem  45776  modelaxreplem2  45802  stoweidlem34  46862  ormklocald  47704  evenwodadd  47729  cfsetsnfsetf1  47947  fcoresf1  47957  euoreqb  47997  2reu8i  48001  ralralimp  48166  f1oresf1o2  48179  zm1nn  48190  elfz2z  48203  2tceilhalfelfzo1  48224  m1modmmod  48252  modlt0b  48257  muldvdsfacgt  48274  muldvdsfacm1  48275  iccpartlt  48324  iccelpart  48333  icceuelpartlem  48335  fargshiftf1  48341  sprsymrelf1lem  48391  paireqne  48411  reuopreuprim  48426  goldbachthlem2  48449  odz2prm2pw  48466  fmtnoprmfac1lem  48467  fmtnofac2lem  48471  prmdvdsfmtnof1  48490  sfprmdvdsmersenne  48506  lighneallem2  48509  lighneallem4  48513  fppr2odd  48647  gbegt5  48677  gbowge7  48679  bgoldbtbndlem4  48724  bgoldbtbnd  48725  tgoldbach  48733  grimuhgr  48803  grimcnv  48804  grimco  48805  isuspgrim0  48810  isuspgrimlem  48811  upgrimwlklem5  48817  upgrimtrlslem2  48821  uhgrimisgrgriclem  48846  clnbgrgrimlem  48849  clnbgrgrim  48850  grimedg  48851  grtriprop  48857  isubgr3stgrlem3  48884  isubgr3stgrlem4  48885  isubgr3stgrlem6  48887  isubgr3stgrlem7  48888  uspgrlimlem3  48906  grlimedgclnbgr  48911  grlimgrtrilem2  48918  grlimgrtri  48919  grlicsym  48929  gpgedgvtx1  48978  gpgedgiov  48981  gpgedg2ov  48982  gpgedg2iv  48983  pgnioedg1  49024  pgnioedg2  49025  pgnioedg3  49026  pgnioedg4  49027  pgnioedg5  49028  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  pgnbgreunbgrlem5lem1  49036  pgnbgreunbgrlem5lem2  49037  pgnbgreunbgrlem5lem3  49038  lcosslsp  49368  lindslinindsimp1  49387  snlindsntor  49401  itcovalt2  49607  eenglngeehlnmlem2  49668  itsclc0yqsol  49694  itschlc0xyqsol1  49696  itschlc0xyqsol  49697  opnneilv  49835  i0oii  49846  io1ii  49847  iscnrm3lem4  49862  iscnrm3r  49874  setrec1lem4  50616  aacllem  50772