Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 29643 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  238  sylbid  239  sylibrd  259  sylbird  260  syland  604  animpimp2impd  845  ax12v2  2174  alrimdd  2208  axc16g  2252  axc16nf  2255  axc11r  2366  sb4a  2480  2eu1  2647  2eu1v  2648  ss2ralv  4052  ss2rexv  4053  trel3  5275  poss  5590  sess2  5645  wefrc  5670  wereu2  5673  predtrss  6321  frpomin  6339  funun  6592  ssimaex  6974  f1cofveqaeq  7254  f1imass  7260  soisoi  7322  isores3  7329  isofrlem  7334  isoselem  7335  weniso  7348  abnexg  7740  oninton  7780  orduniorsuc  7815  limuni3  7838  tfindsg  7847  limom  7868  f1o2ndf1  8105  soxp  8112  xpord3inddlem  8137  soseq  8142  extmptsuppeq  8170  smoel  8357  tfrlem9  8382  tz7.49  8442  seqomlem1  8447  odi  8576  omass  8577  omeulem2  8580  oeordsuc  8591  oeeulem  8598  ertr  8715  swoord2  8732  ecopovtrn  8811  domtriord  9120  pssnn  9165  onomeneqOLD  9226  unxpdomlem2  9248  isinf  9257  isinfOLD  9258  pssnnOLD  9262  f1finf1o  9268  findcard3  9282  findcard3OLD  9283  frfi  9285  unblem3  9294  en3lplem1  9604  inf3lem5  9624  cantnfle  9663  cantnfp1lem3  9672  ttrcltr  9708  frmin  9741  rankxpsuc  9874  tcrank  9876  ficardom  9953  carduni  9973  infxpenlem  10005  dfac8alem  10021  ac10ct  10026  ween  10027  alephdom  10073  alephle  10080  iscard3  10085  alephfp  10100  pwsdompw  10196  infdif  10201  cfslbn  10259  cofsmo  10261  cfcof  10266  fin1a2s  10406  domtriomlem  10434  ac6num  10471  zorn2lem3  10490  axdclem2  10512  imadomg  10526  iundom2g  10532  ficard  10557  fpwwe2lem7  10629  fpwwe2  10635  gchpwdom  10662  gchaclem  10670  tskr1om2  10760  inar1  10767  tskord  10772  tskuni  10775  grudomon  10809  grur1a  10811  grur1  10812  addnidpi  10893  ltexnq  10967  genpnnp  10997  addclprlem2  11009  mulclprlem  11011  psslinpr  11023  ltexprlem6  11033  ltexprlem7  11034  addcanpr  11038  mulgt0sr  11097  map2psrpr  11102  supsrlem  11103  axrrecex  11155  letr  11305  dedekind  11374  recex  11843  lemul12b  12068  mulgt1  12070  fimaxre2  12156  lbreu  12161  nnrecgt0  12252  nnunb  12465  bndndx  12468  zeo  12645  uzind  12651  fzind  12657  fnn0ind  12658  suprfinzcl  12673  suprzcl2  12919  zmax  12926  rpnnen1lem5  12962  xrletr  13134  qbtwnre  13175  qsqueeze  13177  qextltlem  13178  xralrple  13181  xlesubadd  13239  supxrunb1  13295  icoshft  13447  zltaddlt1le  13479  fzen  13515  elfz0fzfz0  13603  elfzmlbp  13609  elfzo0z  13671  fzofzim  13676  fzo1fzo0n0  13680  elfzodifsumelfzo  13695  ssfzoulel  13723  modadd1  13870  modmul1  13886  uzrdgfni  13920  fsuppmapnn0fiub0  13955  fsuppmapnn0ub  13957  fsuppmapnn0fz  13958  seqf1olem1  14004  seqf1olem2  14005  expnbnd  14192  faclbnd4lem4  14253  hashgt23el  14381  seqcoll  14422  hashle2pr  14435  elss2prb  14445  ccatalpha  14540  swrdsbslen  14611  swrdspsleq  14612  swrdswrdlem  14651  swrdswrd  14652  pfxccatin12lem2a  14674  pfxccatin12lem1  14675  pfxccatin12lem3  14679  swrdccat3blem  14686  reuccatpfxs1lem  14693  repswswrd  14731  cshf1  14757  swrd2lsw  14900  sqeqd  15110  sqrmo  15195  cau3lem  15298  icodiamlt  15379  limsupbnd2  15424  lo1bdd2  15465  climuni  15493  rlimcn3  15531  mulcn2  15537  o1of2  15554  rlimo1  15558  lo1le  15595  iseralt  15628  cvgrat  15826  fprodss  15889  rpnnen2lem12  16165  ruclem3  16173  sqrt2irr  16189  p1modz1  16201  dvdsmodexp  16202  dvds2lem  16209  dvdslelem  16249  dvdsabseq  16253  divalglem8  16340  bitsinv1lem  16379  sadcaddlem  16395  smu01lem  16423  smueqlem  16428  bezoutlem4  16481  dfgcd2  16485  algcvga  16513  lcmfunsnlem1  16571  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  lcmfdvdsb  16577  coprmgcdb  16583  coprmdvds2  16588  coprmprod  16595  isprm3  16617  prmdvdsfz  16639  isprm5  16641  coprm  16645  rpexp12i  16658  phibndlem  16700  dfphi2  16704  eulerthlem2  16712  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  17537  initoid  17948  termoid  17949  initoeu2lem1  17961  pospo  18295  dirge  18553  cyccom  19075  gsmsymgrfixlem1  19290  oddvdsnn0  19407  oddvds  19410  odcl2  19428  gexdvds  19447  sylow2alem2  19481  sylow2a  19482  efgi2  19588  efgsrel  19597  efgs1b  19599  imasabl  19739  cyggex2  19760  telgsums  19856  pgpfac1lem2  19940  pgpfac1lem3a  19941  pgpfac1lem3  19942  pgpfac1lem5  19944  lmodfopnelem2  20502  lssssr  20557  gzrngunitlem  21003  znunit  21111  frgpcyg  21121  lsmcss  21237  obselocv  21275  obslbs  21277  mhpvarcl  21683  cply1mul  21810  gsummoncoe1  21820  cpmatacl  22210  cpmatinvcl  22211  cpmatmcllem  22212  m2cpminvid2lem  22248  mp2pm2mplem4  22303  pm2mp  22319  chfacfisf  22348  chfacfisfcpmat  22349  chfacfscmul0  22352  chfacfpmmul0  22356  cayhamlem4  22382  ordtrest2lem  22699  leordtval2  22708  lecldbas  22715  cncls  22770  cncnp  22776  cnpresti  22784  lmcnp  22800  cnt0  22842  isreg2  22873  cmpsublem  22895  cmpsub  22896  tgcmp  22897  bwth  22906  dfconn2  22915  1stcfb  22941  1stcelcls  22957  islly2  22980  dislly  22993  reftr  23010  comppfsc  23028  kgencn2  23053  txcnp  23116  txindis  23130  txcmplem1  23137  txlm  23144  xkohaus  23149  cnmptcom  23174  kqfvima  23226  isr0  23233  fgss2  23370  fbasrn  23380  filuni  23381  ufilmax  23403  isufil2  23404  cfinufil  23424  fmfnfmlem1  23450  fmfnfmlem2  23451  fmfnfmlem4  23453  fmfnfm  23454  fmco  23457  flimopn  23471  hausflim  23477  flimrest  23479  fclsopn  23510  flimfnfcls  23524  alexsubALTlem2  23544  alexsubALTlem3  23545  alexsubALT  23547  ptcmplem2  23549  cnextcn  23563  symgtgp  23602  qustgplem  23617  tsmsres  23640  tsmsxplem1  23649  isucn2  23776  imasdsf1olem  23871  bldisj  23896  blssps  23922  blss  23923  metcnp3  24041  ngptgp  24137  nrginvrcn  24201  nmoleub  24240  xrsmopn  24320  icccmplem3  24332  reconnlem2  24335  rectbntr0  24340  rescncf  24405  iocopnst  24448  iccpnfcnv  24452  lebnumii  24474  nmoleub2lem  24622  nmhmcn  24628  iscfil3  24782  iscau2  24786  iscau3  24787  iscau4  24788  iscmet3lem2  24801  caussi  24806  equivcfil  24808  equivcau  24809  ivthlem2  24961  ivthlem3  24962  ovoliunlem2  25012  ovoliunnul  25016  ioombl1lem4  25070  dyadmax  25107  dyadmbl  25109  volsup2  25114  itg2le  25249  itg2const2  25251  itg2seq  25252  itgsplitioo  25347  rolle  25499  c1lip1  25506  dvivthlem1  25517  lhop1  25523  dvcnvrelem1  25526  dvfsumrlim  25540  ply1divmo  25645  ig1peu  25681  plypf1  25718  coeaddlem  25755  fta1  25813  quotcan  25814  aalioulem4  25840  ulmcaulem  25898  ulmcn  25903  pilem2  25956  sincosq1lem  25999  sinq12gt0  26009  sinq12ge0  26010  tanord1  26038  lognegb  26090  logrec  26258  logbgcd1irr  26289  dcubic  26341  xrlimcnp  26463  o1cxp  26469  ftalem2  26568  ftalem3  26569  fsumdvdscom  26679  chtub  26705  vmasum  26709  bcmono  26770  bposlem3  26779  bposlem7  26783  lgsdir  26825  lgsqrlem2  26840  lgsqrmodndvds  26846  gausslemma2dlem6  26865  gausslemma2d  26867  lgsquadlem2  26874  2lgslem3a1  26893  2lgslem3b1  26894  2lgslem3c1  26895  2lgslem3d1  26896  2sqlem6  26916  2sq2  26926  2sqmod  26929  dchrisumlem3  26984  pntrsumbnd2  27060  pntpbnd1  27079  pntibnd  27086  pntlem3  27102  pntleml  27104  sltres  27155  nosepon  27158  nolesgn2o  27164  nogesgn1o  27166  nodenselem8  27184  nosupbnd1lem1  27201  madess  27361  madebdaylemlrcut  27383  brbtwn2  28153  colinearalg  28158  axcontlem10  28221  edgupgr  28384  edglnl  28393  usgruspgrb  28431  subupgr  28534  uhgrspan1  28550  usgredgsscusgredg  28706  fusgrn0degnn0  28746  upgrewlkle2  28853  uspgr2wlkeq  28893  redwlk  28919  wlkdlem2  28930  upgrwlkdvdelem  28983  pthdlem1  29013  pthdlem2  29015  crctcshwlkn0lem3  29056  wlkiswwlks1  29111  wwlksm1edg  29125  wwlksnred  29136  wwlksnextbi  29138  umgr2adedgspth  29192  clwlkclwwlklem2fv2  29239  clwlkclwwlklem2a  29241  clwlkclwwlkf1lem3  29249  clwwisshclwwslemlem  29256  clwwlkf  29290  clwwlkext2edg  29299  wwlksubclwwlk  29301  clwwlknonex2lem2  29351  eupth2lems  29481  frgrwopreglem4a  29553  frgrregorufrg  29569  ex-natded5.3-2  29651  isgrpo  29738  vacn  29935  ubthlem2  30112  htthlem  30158  normgt0  30368  shmodsi  30630  spansneleq  30811  h1datomi  30822  nmcexi  31267  pjnormssi  31409  stm1add3i  31488  golem2  31513  cvnsym  31531  dmdmd  31541  mdslmd1lem1  31566  mdslmd1i  31570  mdexchi  31576  atcveq0  31589  superpos  31595  hatomistici  31603  atoml2i  31624  atcvat2i  31628  chirredlem1  31631  atcvat3i  31637  mdsymlem3  31646  mdsymlem5  31648  cdj3lem2b  31678  cdj3i  31682  supssd  31922  infssd  31923  resspos  32124  resstos  32125  submarchi  32320  tpr2rico  32881  ordtrest2NEWlem  32891  xrge0iifcnv  32902  omssubadd  33288  eulerpartlemb  33356  ballotlemfc0  33480  ballotlemfcc  33481  ftc2re  33599  loop1cycl  34117  subfacp1lem6  34165  iccllysconn  34230  cvmfolem  34259  satfsschain  34344  satfrel  34347  satfdm  34349  sat1el2xp  34359  satffunlem1lem1  34382  dmopab3rexdif  34385  satffunlem2lem2  34386  satffun  34389  fundmpss  34727  dfon2lem3  34746  dfon2lem6  34749  axextbdist  34761  dfrdg4  34912  5segofs  34967  cgrextend  34969  segconeu  34972  btwncomim  34974  btwnswapid  34978  btwnintr  34980  btwnexch3  34981  btwndiff  34988  ifscgr  35005  cgrxfr  35016  btwnxfr  35017  lineext  35037  brofs2  35038  linecgr  35042  lineid  35044  idinside  35045  endofsegid  35046  btwnconn1lem13  35060  btwnconn3  35064  finminlem  35192  nn0prpwlem  35196  cldbnd  35200  clsint2  35203  fnessref  35231  neibastop3  35236  fgmin  35244  onsuct0  35315  limsucncmpi  35319  bj-nnfea  35601  bj-axc14  35724  bj-restn0  35960  bj-0int  35971  wl-19.2reqv  36382  wl-aetr  36387  wl-axc11r  36388  fin2so  36464  tan2h  36469  lindsenlbs  36472  poimirlem2  36479  poimirlem9  36486  poimirlem17  36494  poimirlem18  36495  poimirlem21  36498  poimirlem23  36500  poimirlem26  36503  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimir  36510  heicant  36512  mblfinlem2  36515  mblfinlem3  36516  itg2addnclem  36528  itg2addnclem2  36529  itg2gt0cn  36532  ftc1anclem5  36554  ftc1anclem6  36555  filbcmb  36597  nninfnub  36608  mettrifi  36614  geomcau  36616  istotbnd3  36628  sstotbnd2  36631  ismtybndlem  36663  heibor1lem  36666  heiborlem1  36668  heiborlem8  36675  heiborlem10  36677  heibor  36678  opidonOLD  36709  riscer  36845  crngohomfo  36863  keridl  36889  ispridl2  36895  ispridlc  36927  ac6s6  37029  eqvreltr  37466  dral1-o  37763  ax12indalem  37804  ax12inda2ALT  37805  lsatcveq0  37891  eqlkr3  37960  atlatmstc  38178  atlrelat1  38180  hlrelat2  38263  intnatN  38267  cvrexchlem  38279  cvratlem  38281  cvrat2  38289  atltcvr  38295  cvrat3  38302  cvrat4  38303  ps-1  38337  ps-2  38338  lplnnle2at  38401  lvolnle3at  38442  2llnma3r  38648  cdlemblem  38653  pmapjoin  38712  elpcliN  38753  lhpmcvr4N  38886  4atexlemnclw  38930  trlnidatb  39037  cdlemc4  39054  cdlemd3  39060  cdleme3g  39094  cdleme7d  39106  cdleme11c  39121  cdleme11dN  39122  cdleme21b  39186  cdleme21c  39187  cdleme21i  39195  cdleme22b  39201  cdleme35fnpq  39309  cdlemf1  39421  trlord  39429  cdlemg6c  39480  dihglblem6  40200  dochlkr  40245  dochkrshp  40246  dihjat1lem  40288  dochexmidlem5  40324  dochexmidlem8  40327  metakunt29  41002  qsalrel  41060  remulcand  41308  prjspner1  41365  fphpdo  41541  pellexlem5  41557  pellexlem6  41558  jm2.26lem3  41726  unxpwdom3  41823  omlimcl2  41977  oe0suclim  42013  cantnfresb  42060  tfsconcatb0  42080  naddsuc2  42129  naddgeoa  42131  iscard5  42273  sqrtcval  42378  ov2ssiunov2  42437  frege124d  42498  ordpss  43196  19.41rg  43297  stoweidlem34  44737  cfsetsnfsetf1  45756  fcoresf1  45766  euoreqb  45804  2reu8i  45808  ralralimp  45973  f1oresf1o2  45986  zm1nn  45997  elfz2z  46010  iccpartlt  46079  iccelpart  46088  icceuelpartlem  46090  fargshiftf1  46096  sprsymrelf1lem  46146  paireqne  46166  reuopreuprim  46181  goldbachthlem2  46201  odz2prm2pw  46218  fmtnoprmfac1lem  46219  fmtnofac2lem  46223  prmdvdsfmtnof1  46242  sfprmdvdsmersenne  46258  lighneallem2  46261  lighneallem4  46265  fppr2odd  46386  gbegt5  46416  gbowge7  46418  bgoldbtbndlem4  46463  bgoldbtbnd  46464  tgoldbach  46472  isomuspgrlem2b  46484  isomgrsym  46491  rnglidlmcl  46733  zrtermorngc  46853  zrtermoringc  46922  lcosslsp  47073  lindslinindsimp1  47092  snlindsntor  47106  m1modmmod  47161  itcovalt2  47317  eenglngeehlnmlem2  47378  itsclc0yqsol  47404  itschlc0xyqsol1  47406  itschlc0xyqsol  47407  opnneilv  47495  i0oii  47506  io1ii  47507  iscnrm3lem4  47523  iscnrm3r  47535  setrec1lem4  47689  aacllem  47802