Theorem syld 48

Description: Syllogism deduction. Deduction associated with syl 18. See conventions 30994 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  2251  axc16g  2295  axc16nf  2298  axc11r  2398  sb4a  2510  2eu1  2676  2eu1v  2677  ss2ralv  4002  ss2rexv  4003  trel3  5221  poss  5561  sess2  5617  wefrc  5645  wereu2  5648  predtrss  6324  frpomin  6342  ordpss  6390  funun  6584  ssimaex  6968  f1cofveqaeq  7259  f1imass  7266  soisoi  7334  isores3  7341  isofrlem  7346  isoselem  7347  weniso  7362  abnexg  7768  oninton  7807  orduniorsuc  7839  limuni3  7861  tfindsg  7870  limom  7891  resf1extb  7944  f1o2ndf1  8131  soxp  8139  xpord3inddlem  8164  soseq  8169  extmptsuppeq  8198  smoel  8361  tfrlem9  8386  tz7.49  8448  seqomlem1  8453  odi  8580  omass  8581  omeulem2  8584  oeordsuc  8596  oeeulem  8603  naddsuc2  8704  ertr  8726  swoord2  8744  ecopovtrn  8834  domtriord  9135  pssnn  9177  unxpdomlem2  9241  isinf  9249  f1finf1o  9257  findcard3  9267  frfi  9269  fissorduni  9275  unblem3  9279  supssd  9448  infssd  9479  en3lplem1  9606  inf3lem5  9626  cantnfle  9665  cantnfp1lem3  9674  ttrcltr  9710  frmin  9746  rankxpsuc  9892  tcrank  9894  setrec1lem4  9964  ficardom  10035  carduni  10055  infxpenlem  10085  dfac8alem  10101  ac10ct  10106  ween  10107  alephdom  10153  alephle  10160  iscard3  10165  alephfp  10180  pwsdompw  10274  infdif  10279  cfslbn  10338  cofsmo  10340  cfcof  10345  fin1a2s  10485  domtriomlem  10513  ac6num  10550  zorn2lem3  10569  axdclem2  10591  imadomg  10606  iundom2g  10617  ficard  10642  fpwwe2lem7  10715  fpwwe2  10721  gchpwdom  10748  gchaclem  10756  tskhf  10846  inar1  10853  tskord  10858  tskuni  10861  grudomon  10895  grur1a  10897  grur1  10898  addnidpi  10979  ltexnq  11053  genpnnp  11083  addclprlem2  11095  mulclprlem  11097  psslinpr  11109  ltexprlem6  11119  ltexprlem7  11120  addcanpr  11124  mulgt0sr  11183  map2psrpr  11188  supsrlem  11189  axrrecex  11241  letr  11397  dedekind  11466  recex  11941  lemul12b  12167  fimaxre2  12255  lbreu  12260  nnrecgt0  12374  nnunb  12595  bndndx  12598  zeo  12778  uzind  12784  fzind  12790  fnn0ind  12791  suprfinzcl  12806  suprzcl2  13058  zmax  13065  rpnnen1lem5  13102  xrletr  13280  qbtwnre  13322  qsqueeze  13324  qextltlem  13325  xralrple  13328  xlesubadd  13386  supxrunb1  13442  icoshft  13597  zltaddlt1le  13629  fzen  13667  elfz0fzfz0  13760  elfzmlbp  13766  elfzo0z  13829  fzofzim  13837  fzo1fzo0n0  13843  elfzodifsumelfzo  13859  ssfzoulel  13888  modadd1  14041  modmul1  14060  uzrdgfni  14094  fsuppmapnn0fiub0  14129  fsuppmapnn0ub  14131  fsuppmapnn0fz  14132  seqf1olem1  14177  seqf1olem2  14178  expnbnd  14369  faclbnd4lem4  14433  hashgt23el  14562  seqcoll  14602  hashle2pr  14615  elss2prb  14626  ccatalpha  14733  swrdsbslen  14807  swrdspsleq  14808  swrdswrdlem  14846  swrdswrd  14847  pfxccatin12lem2a  14869  pfxccatin12lem1  14870  pfxccatin12lem3  14874  swrdccat3blem  14881  reuccatpfxs1lem  14888  repswswrd  14928  cshf1  14954  swrd2lsw  15098  sqeqd  15326  sqrmo  15411  cau3lem  15515  icodiamlt  15598  limsupbnd2  15643  lo1bdd2  15684  climuni  15712  rlimcn3  15750  mulcn2  15756  o1of2  15773  rlimo1  15777  lo1le  15812  iseralt  15845  cvgrat  16045  fprodss  16108  rpnnen2lem12  16386  ruclem3  16394  sqrt2irr  16410  p1modz1  16422  dvdsmodexp  16423  dvds2lem  16431  dvdslelem  16472  dvdsabseq  16476  divalglem8  16563  bitsinv1lem  16604  sadcaddlem  16620  smu01lem  16648  smueqlem  16653  bezoutlem4  16708  dfgcd2  16712  algcvga  16747  lcmfunsnlem1  16805  lcmfunsnlem2lem1  16806  lcmfunsnlem2lem2  16807  lcmfdvdsb  16811  coprmgcdb  16817  coprmdvds2  16822  coprmprod  16829  isprm3  16851  prmdvdsfz  16874  isprm5  16876  coprm  16880  rpexp12i  16893  phibndlem  16940  dfphi2  16944  eulerthlem2  16952  odzdvds  16966  iserodd  17006  pclem  17009  pcpremul  17014  pcqcl  17027  pcdvdsb  17040  pcprmpw2  17053  difsqpwdvds  17058  pcaddlem  17059  pcmptcl  17062  pcfac  17070  prmpwdvds  17075  unbenlem  17079  prmreclem1  17087  4sqlem17  17132  vdwmc2  17150  vdwlem9  17160  vdwlem10  17161  vdwlem13  17164  vdwnnlem3  17168  ramcl  17200  prmgaplem7  17228  mreiincl  17759  initoid  18169  termoid  18170  initoeu2lem1  18182  pospo  18510  resspos  18596  resstos  18597  dirge  18770  mgmidpfod  18850  cyccom  19411  gsmsymgrfixlem1  19634  oddvdsnn0  19751  oddvds  19754  odcl2  19772  gexdvds  19791  sylow2alem2  19825  sylow2a  19826  efgi2  19932  efgsrel  19941  efgs1b  19943  imasabl  20083  cyggex2  20104  telgsums  20200  pgpfac1lem2  20284  pgpfac1lem3a  20285  pgpfac1lem3  20286  pgpfac1lem5  20288  crngrhmfo  20719  zrtermorngc  20888  zrtermoringc  20920  lmodfopnelem2  21167  lssssr  21222  rnglidlmcl  21488  unichnlidl  21509  gzrngunitlem  21731  znunit  21862  frgpcyg  21872  lsmcss  21991  obselocv  22027  obslbs  22029  lindsenlbs  22150  mhpvarcl  22462  cply1mul  22607  gsummoncoe1  22619  cpmatacl  23027  cpmatinvcl  23028  cpmatmcllem  23029  m2cpminvid2lem  23065  mp2pm2mplem4  23120  pm2mp  23136  chfacfisf  23165  chfacfisfcpmat  23166  chfacfscmul0  23169  chfacfpmmul0  23173  cayhamlem4  23199  ordtrest2lem  23514  leordtval2  23523  lecldbas  23530  cncls  23585  cncnp  23591  cnpresti  23599  lmcnp  23615  cnt0  23657  isreg2  23688  cmpsublem  23710  cmpsub  23711  tgcmp  23712  bwth  23721  dfconn2  23730  1stcfb  23756  1stcelcls  23773  islly2  23796  dislly  23809  reftr  23826  comppfsc  23844  kgencn2  23869  txcnp  23932  txindis  23946  txcmplem1  23953  txlm  23960  xkohaus  23965  cnmptcom  23990  kqfvima  24042  isr0  24049  fgss2  24186  fbasrn  24196  filuni  24197  ufilmax  24219  isufil2  24220  cfinufil  24240  fmfnfmlem1  24266  fmfnfmlem2  24267  fmfnfmlem4  24269  fmfnfm  24270  fmco  24273  flimopn  24287  hausflim  24293  flimrest  24295  fclsopn  24326  flimfnfcls  24340  alexsubALTlem2  24360  alexsubALTlem3  24361  alexsubALT  24363  ptcmplem2  24365  cnextcn  24379  symgtgp  24418  qustgplem  24433  tsmsres  24456  tsmsxplem1  24465  isucn2  24590  imasdsf1olem  24685  bldisj  24710  blssps  24736  blss  24737  metcnp3  24852  ngptgp  24948  nrginvrcn  25004  nmoleub  25043  xrsmopn  25125  icccmplem3  25137  reconnlem2  25140  rectbntr0  25145  rescncf  25211  iocopnst  25254  iccpnfcnv  25258  lebnumii  25280  nmoleub2lem  25428  nmhmcn  25434  iscfil3  25587  iscau2  25591  iscau3  25592  iscau4  25593  iscmet3lem2  25606  caussi  25611  equivcfil  25613  equivcau  25614  ivthlem2  25766  ivthlem3  25767  ovoliunlem2  25817  ovoliunnul  25821  ioombl1lem4  25875  dyadmax  25912  dyadmbl  25914  volsup2  25919  itg2le  26053  itg2const2  26055  itg2seq  26056  itgsplitioo  26151  rolle  26303  c1lip1  26310  dvivthlem1  26321  lhop1  26327  dvcnvrelem1  26330  dvfsumrlim  26344  ply1divmo  26447  ig1peu  26486  plypf1  26524  coeaddlem  26561  dvply2g  26599  fta1  26622  quotcan  26625  aalioulem4  26655  ulmcaulem  26714  ulmcn  26719  pilem2  26772  sincosq1lem  26819  sinq12gt0  26829  sinq12ge0  26830  tanord1  26858  lognegb  26911  logrec  27084  logbgcd1irr  27115  dcubic  27167  xrlimcnp  27289  o1cxp  27295  ftalem2  27394  ftalem3  27395  fsumdvdscom  27505  chtub  27532  vmasum  27536  bcmono  27597  bposlem3  27606  bposlem7  27610  lgsdir  27652  lgsqrlem2  27667  lgsqrmodndvds  27673  gausslemma2dlem6  27692  gausslemma2d  27694  lgsquadlem2  27701  2lgslem3a1  27720  2lgslem3b1  27721  2lgslem3c1  27722  2lgslem3d1  27723  2sqlem6  27743  2sq2  27753  2sqmod  27756  dchrisumlem3  27811  pntrsumbnd2  27887  pntpbnd1  27906  pntibnd  27913  pntlem3  27929  pntleml  27931  fltoprm  27988  ltsres  28012  nosepon  28015  nolesgn2o  28021  nogesgn1o  28023  nodenselem8  28041  nosupbnd1lem1  28058  madess  28245  madebdaylemlrcut  28278  peano5uzs  28783  bdayfinbndlem1  28846  z12bday  28864  brbtwn2  29476  colinearalg  29481  axcontlem10  29544  edgupgr  29705  edglnl  29714  usgruspgrb  29757  subupgr  29861  uhgrspan1  29877  usgredgsscusgredg  30033  fusgrn0degnn0  30073  upgrewlkle2  30180  uspgr2wlkeq  30219  redwlk  30244  wlkdlem2  30255  upgrwlkdvdelem  30315  pthdlem1  30345  pthdlem2  30347  crctcshwlkn0lem3  30394  wlkiswwlks1  30449  wwlksm1edg  30463  wwlksnred  30474  wwlksnextbi  30476  umgr2adedgspth  30530  clwlkclwwlklem2fv2  30580  clwlkclwwlklem2a  30582  clwlkclwwlkf1lem3  30590  clwwisshclwwslemlem  30597  clwwlkf  30631  clwwlkext2edg  30640  wwlksubclwwlk  30642  clwwlknonex2lem2  30692  loop1cycl  30737  eupth2lems  30832  frgrwopreglem4a  30904  frgrregorufrg  30920  ex-natded5.3-2  31002  isgrpo  31092  vacn  31289  ubthlem2  31466  htthlem  31512  normgt0  31722  shmodsi  31984  spansneleq  32165  h1datomi  32176  nmcexi  32621  pjnormssi  32763  stm1add3i  32842  golem2  32867  cvnsym  32885  dmdmd  32895  mdslmd1lem1  32920  mdslmd1i  32924  mdexchi  32930  atcveq0  32943  superpos  32949  hatomistici  32957  atoml2i  32978  atcvat2i  32982  chirredlem1  32985  atcvat3i  32991  mdsymlem3  33000  mdsymlem5  33002  cdj3lem2b  33032  cdj3i  33036  submarchi  33740  dfufd2  34075  tpr2rico  34537  ordtrest2NEWlem  34547  xrge0iifcnv  34558  omssubadd  34925  eulerpartlemb  34993  ballotlemfc0  35118  ballotlemfcc  35119  ftc2re  35220  fineqvinfep  35776  axsepg2  35791  axsepg4  35794  axpowg2  35798  axpowg3  35799  subfacp1lem6  35929  iccllysconn  35994  cvmfolem  36023  satfsschain  36108  satfrel  36111  satfdm  36113  sat1el2xp  36123  satffunlem1lem1  36146  dmopab3rexdif  36149  satffunlem2lem2  36150  satffun  36153  fundmpss  36511  dfon2lem3  36527  dfon2lem6  36530  axextbdist  36542  dfrdg4  36695  5segofs  36751  cgrextend  36753  segconeu  36756  btwncomim  36758  btwnswapid  36762  btwnintr  36764  btwnexch3  36765  btwndiff  36772  ifscgr  36789  cgrxfr  36800  btwnxfr  36801  lineext  36821  brofs2  36822  linecgr  36826  lineid  36828  idinside  36829  endofsegid  36830  btwnconn1lem13  36844  btwnconn3  36848  finminlem  37086  nn0prpwlem  37090  cldbnd  37094  clsint2  37097  fnessref  37125  neibastop3  37130  fgmin  37138  onsuct0  37209  limsucncmpi  37213  tr0elw  37252  tr0el  37253  bj-nnfea  37616  bj-axc14  37748  bj-restn0  37991  bj-0int  38002  wl-19.2reqv  38436  wl-aetr  38441  wl-axc11r  38442  fin2so  38510  tan2h  38515  poimirlem2  38520  poimirlem9  38527  poimirlem17  38535  poimirlem18  38536  poimirlem21  38539  poimirlem23  38541  poimirlem26  38544  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  poimir  38551  heicant  38553  mblfinlem2  38556  mblfinlem3  38557  itg2addnclem  38569  itg2addnclem2  38570  itg2gt0cn  38573  ftc1anclem5  38595  ftc1anclem6  38596  findcard4  38612  dfprop2  38626  filbcmb  38654  nninfnub  38665  mettrifi  38671  geomcau  38673  istotbnd3  38685  sstotbnd2  38688  ismtybndlem  38720  heibor1lem  38723  heiborlem1  38725  heiborlem8  38732  heiborlem10  38734  heibor  38735  opidonOLD  38766  riscer  38902  crngohomfo  38920  keridl  38946  ispridl2  38952  ispridlc  38984  ac6s6  39084  eqvreltr  39603  eldisjdmqsim  39729  suceldisj  39730  eldisjs6  39852  dral1-o  39941  ax12indalem  39982  ax12inda2ALT  39983  lsatcveq0  40069  eqlkr3  40138  atlatmstc  40356  atlrelat1  40358  hlrelat2  40440  intnatN  40444  cvrexchlem  40456  cvratlem  40458  cvrat2  40466  atltcvr  40472  cvrat3  40479  cvrat4  40480  ps-1  40514  ps-2  40515  lplnnle2at  40578  lvolnle3at  40619  2llnma3r  40825  cdlemblem  40830  pmapjoin  40889  elpcliN  40930  lhpmcvr4N  41063  4atexlemnclw  41107  trlnidatb  41214  cdlemc4  41231  cdlemd3  41237  cdleme3g  41271  cdleme7d  41283  cdleme11c  41298  cdleme11dN  41299  cdleme21b  41363  cdleme21c  41364  cdleme21i  41372  cdleme22b  41378  cdleme35fnpq  41486  cdlemf1  41598  trlord  41606  cdlemg6c  41657  dihglblem6  42377  dochlkr  42422  dochkrshp  42423  dihjat1lem  42465  dochexmidlem5  42501  dochexmidlem8  42504  qsalrel  43272  remulcand  43470  fphpdo  43803  pellexlem5  43819  pellexlem6  43820  jm2.26lem3  43987  unxpwdom3  44081  omlimcl2  44228  oe0suclim  44263  cantnfresb  44310  tfsconcatb0  44330  naddgeoa  44380  iscard5  44521  sqrtcval  44626  ov2ssiunov2  44685  frege124d  44746  19.41rg  45518  relpfrlem  45921  modelaxreplem2  45947  stoweidlem34  47013  ormklocald  47855  evenwodadd  47880  cfsetsnfsetf1  48098  fcoresf1  48108  euoreqb  48148  2reu8i  48152  ralralimp  48317  f1oresf1o2  48330  zm1nn  48341  elfz2z  48354  2tceilhalfelfzo1  48375  m1modmmod  48403  modlt0b  48408  muldvdsfacgt  48425  muldvdsfacm1  48426  iccpartlt  48475  iccelpart  48484  icceuelpartlem  48486  fargshiftf1  48492  sprsymrelf1lem  48542  paireqne  48562  reuopreuprim  48577  goldbachthlem2  48600  odz2prm2pw  48617  fmtnoprmfac1lem  48618  fmtnofac2lem  48622  prmdvdsfmtnof1  48641  sfprmdvdsmersenne  48657  lighneallem2  48660  lighneallem4  48664  fppr2odd  48798  gbegt5  48828  gbowge7  48830  bgoldbtbndlem4  48875  bgoldbtbnd  48876  tgoldbach  48884  grimuhgr  48954  grimcnv  48955  grimco  48956  isuspgrim0  48961  isuspgrimlem  48962  upgrimwlklem5  48968  upgrimtrlslem2  48972  uhgrimisgrgriclem  48997  clnbgrgrimlem  49000  clnbgrgrim  49001  grimedg  49002  grtriprop  49008  isubgr3stgrlem3  49035  isubgr3stgrlem4  49036  isubgr3stgrlem6  49038  isubgr3stgrlem7  49039  uspgrlimlem3  49057  grlimedgclnbgr  49062  grlimgrtrilem2  49069  grlimgrtri  49070  grlicsym  49080  gpgedgvtx1  49129  gpgedgiov  49132  gpgedg2ov  49133  gpgedg2iv  49134  pgnioedg1  49175  pgnioedg2  49176  pgnioedg3  49177  pgnioedg4  49178  pgnioedg5  49179  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  pgnbgreunbgrlem5lem1  49187  pgnbgreunbgrlem5lem2  49188  pgnbgreunbgrlem5lem3  49189  lcosslsp  49519  lindslinindsimp1  49538  snlindsntor  49552  itcovalt2  49758  eenglngeehlnmlem2  49819  itsclc0yqsol  49845  itschlc0xyqsol1  49847  itschlc0xyqsol  49848  opnneilv  49986  i0oii  49997  io1ii  49998  iscnrm3lem4  50013  iscnrm3r  50025  aacllem  50908