Theorem syld 48

Description: Syllogism deduction. Deduction associated with syl 18. See conventions 31058 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  2218  alrimdd  2254  axc16g  2298  axc16nf  2301  axc11r  2400  sb4a  2512  2eu1  2678  2eu1v  2679  ss2ralv  3984  ss2rexv  3985  trel3  5227  poss  5568  sess2  5624  wefrc  5652  wereu2  5655  predtrss  6351  frpomin  6369  ordpss  6417  funun  6614  ssimaex  7001  f1cofveqaeq  7292  f1imass  7299  soisoi  7367  isores3  7374  isofrlem  7379  isoselem  7380  weniso  7395  abnexg  7802  oninton  7843  orduniorsuc  7875  limuni3  7897  tfindsg  7906  limom  7927  resf1extb  7980  f1o2ndf1  8170  soxp  8178  xpord3inddlem  8208  soseq  8213  extmptsuppeq  8243  smoel  8406  tfrlem9  8431  tz7.49  8493  seqomlem1  8498  odi  8625  omass  8626  omeulem2  8629  oeordsuc  8641  oeeulem  8648  naddsuc2  8749  ertr  8771  swoord2  8789  ecopovtrn  8879  domtriord  9180  pssnn  9222  unxpdomlem2  9286  isinf  9294  f1finf1o  9302  findcard3  9312  frfi  9314  fissorduni  9320  unblem3  9324  supssd  9492  infssd  9523  en3lplem1  9650  inf3lem5  9670  cantnfle  9709  cantnfp1lem3  9718  ttrcltr  9754  frmin  9790  rankxpsuc  9936  tcrank  9938  setrec1lem4  10008  ficardom  10079  carduni  10101  infxpenlem  10131  dfac8alem  10147  ac10ct  10152  ween  10153  alephdom  10199  alephle  10206  iscard3  10211  alephfp  10226  pwsdompw  10320  infdif  10325  cfslbn  10384  cofsmo  10386  cfcof  10391  fin1a2s  10531  domtriomlem  10559  ac6num  10596  zorn2lem3  10615  axdclem2  10637  imadomg  10652  iundom2g  10663  ficard  10688  fpwwe2lem7  10761  fpwwe2  10767  gchpwdom  10794  gchaclem  10802  tskhf  10892  inar1  10899  tskord  10904  tskuni  10907  grudomon  10941  grur1a  10943  grur1  10944  addnidpi  11025  ltexnq  11099  genpnnp  11129  addclprlem2  11141  mulclprlem  11143  psslinpr  11155  ltexprlem6  11165  ltexprlem7  11166  addcanpr  11170  mulgt0sr  11229  map2psrpr  11234  supsrlem  11235  axrrecex  11287  dedekind  11512  recex  11988  lemul12b  12214  fimaxre2  12302  lbreu  12307  nnrecgt0  12421  nnunb  12642  bndndx  12645  zeo  12825  uzind  12831  fzind  12837  fnn0ind  12838  suprfinzcl  12853  suprzcl2  13105  zmax  13112  rpnnen1lem5  13149  xrletr  13327  qbtwnre  13369  qsqueeze  13371  qextltlem  13372  xralrple  13375  xlesubadd  13433  supxrunb1  13489  icoshft  13644  zltaddlt1le  13676  fzen  13714  elfz0fzfz0  13807  elfzmlbp  13813  elfzo0z  13876  fzofzim  13884  fzo1fzo0n0  13890  elfzodifsumelfzo  13906  ssfzoulel  13935  modadd1  14088  modmul1  14107  uzrdgfni  14141  fsuppmapnn0fiub0  14176  fsuppmapnn0ub  14178  fsuppmapnn0fz  14179  seqf1olem1  14224  seqf1olem2  14225  expnbnd  14417  faclbnd4lem4  14481  hashgt23el  14610  seqcoll  14650  hashle2pr  14663  elss2prb  14674  ccatalpha  14781  swrdsbslen  14856  swrdspsleq  14857  swrdswrdlem  14895  swrdswrd  14896  pfxccatin12lem2a  14918  pfxccatin12lem1  14919  pfxccatin12lem3  14923  swrdccat3blem  14930  reuccatpfxs1lem  14937  repswswrd  14977  cshf1  15003  swrd2lsw  15148  sqeqd  15376  sqrmo  15461  cau3lem  15566  icodiamlt  15649  limsupbnd2  15694  lo1bdd2  15735  climuni  15763  rlimcn3  15801  mulcn2  15807  o1of2  15824  rlimo1  15828  lo1le  15863  iseralt  15896  cvgrat  16096  fprodss  16159  rpnnen2lem12  16437  ruclem3  16445  sqrt2irr  16461  p1modz1  16473  dvdsmodexp  16474  dvds2lem  16482  dvdslelem  16523  dvdsabseq  16527  divalglem8  16614  bitsinv1lem  16655  sadcaddlem  16671  smu01lem  16699  smueqlem  16704  bezoutlem4  16759  dfgcd2  16763  algcvga  16798  lcmfunsnlem1  16856  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfdvdsb  16862  coprmgcdb  16868  coprmdvds2  16873  coprmprod  16880  isprm3  16902  prmdvdsfz  16925  isprm5  16927  coprm  16931  rpexp12i  16944  phibndlem  16991  dfphi2  16995  eulerthlem2  17003  odzdvds  17017  iserodd  17057  pclem  17060  pcpremul  17065  pcqcl  17078  pcdvdsb  17091  pcprmpw2  17104  difsqpwdvds  17109  pcaddlem  17110  pcmptcl  17113  pcfac  17121  prmpwdvds  17126  unbenlem  17130  prmreclem1  17138  4sqlem17  17183  vdwmc2  17201  vdwlem9  17211  vdwlem10  17212  vdwlem13  17215  vdwnnlem3  17219  ramcl  17251  prmgaplem7  17279  mreiincl  17816  initoid  18226  termoid  18227  initoeu2lem1  18239  pospo  18567  resspos  18653  resstos  18654  dirge  18827  mgmidpfod  18907  cyccom  19468  gsmsymgrfixlem1  19692  oddvdsnn0  19809  oddvds  19812  odcl2  19830  gexdvds  19849  sylow2alem2  19883  sylow2a  19884  efgi2  19990  efgsrel  19999  efgs1b  20001  imasabl  20141  cyggex2  20162  telgsums  20258  pgpfac1lem2  20342  pgpfac1lem3a  20343  pgpfac1lem3  20344  pgpfac1lem5  20346  crngrhmfo  20777  zrtermorngc  20946  zrtermoringc  20978  lmodfopnelem2  21225  lssssr  21280  rnglidlmcl  21546  unichnlidl  21567  gzrngunitlem  21792  znunit  21924  frgpcyg  21934  lsmcss  22053  obselocv  22089  obslbs  22091  lindsenlbs  22212  mhpvarcl  22524  cply1mul  22669  gsummoncoe1  22681  cpmatacl  23089  cpmatinvcl  23090  cpmatmcllem  23091  m2cpminvid2lem  23127  mp2pm2mplem4  23182  pm2mp  23198  chfacfisf  23227  chfacfisfcpmat  23228  chfacfscmul0  23231  chfacfpmmul0  23235  cayhamlem4  23261  ordtrest2lem  23576  leordtval2  23585  lecldbas  23592  cncls  23647  cncnp  23653  cnpresti  23661  lmcnp  23677  cnt0  23719  isreg2  23750  cmpsublem  23772  cmpsub  23773  tgcmp  23774  bwth  23783  dfconn2  23792  1stcfb  23818  1stcelcls  23835  islly2  23858  dislly  23871  reftr  23888  comppfsc  23906  kgencn2  23931  txcnp  23994  txindis  24008  txcmplem1  24015  txlm  24022  xkohaus  24027  cnmptcom  24052  kqfvima  24104  isr0  24111  fgss2  24248  fbasrn  24258  filuni  24259  ufilmax  24281  isufil2  24282  cfinufil  24302  fmfnfmlem1  24328  fmfnfmlem2  24329  fmfnfmlem4  24331  fmfnfm  24332  fmco  24335  flimopn  24349  hausflim  24355  flimrest  24357  fclsopn  24388  flimfnfcls  24402  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALT  24425  ptcmplem2  24427  cnextcn  24441  symgtgp  24480  qustgplem  24495  tsmsres  24518  tsmsxplem1  24527  isucn2  24652  imasdsf1olem  24747  bldisj  24772  blssps  24798  blss  24799  metcnp3  24914  ngptgp  25010  nrginvrcn  25066  nmoleub  25105  xrsmopn  25187  icccmplem3  25199  reconnlem2  25202  rectbntr0  25207  rescncf  25273  iocopnst  25316  iccpnfcnv  25320  lebnumii  25342  nmoleub2lem  25490  nmhmcn  25496  iscfil3  25649  iscau2  25653  iscau3  25654  iscau4  25655  iscmet3lem2  25668  caussi  25673  equivcfil  25675  equivcau  25676  ivthlem2  25828  ivthlem3  25829  ovoliunlem2  25879  ovoliunnul  25883  ioombl1lem4  25937  dyadmax  25974  dyadmbl  25976  volsup2  25981  itg2le  26115  itg2const2  26117  itg2seq  26118  itgsplitioo  26213  rolle  26365  c1lip1  26372  dvivthlem1  26383  lhop1  26389  dvcnvrelem1  26392  dvfsumrlim  26406  ply1divmo  26509  ig1peu  26548  plypf1  26586  coeaddlem  26623  dvply2g  26661  fta1  26684  quotcan  26687  aalioulem4  26719  ulmcaulem  26778  ulmcn  26783  pilem2  26836  sincosq1lem  26883  sinq12gt0  26893  sinq12ge0  26894  tanord1  26922  lognegb  26975  logrec  27148  logbgcd1irr  27179  dcubic  27231  xrlimcnp  27353  o1cxp  27359  ftalem2  27458  ftalem3  27459  fsumdvdscom  27569  chtub  27596  vmasum  27600  bcmono  27661  bposlem3  27670  bposlem7  27674  lgsdir  27716  lgsqrlem2  27731  lgsqrmodndvds  27737  gausslemma2dlem6  27756  gausslemma2d  27758  lgsquadlem2  27765  2lgslem3a1  27784  2lgslem3b1  27785  2lgslem3c1  27786  2lgslem3d1  27787  2sqlem6  27807  2sq2  27817  2sqmod  27820  dchrisumlem3  27875  pntrsumbnd2  27951  pntpbnd1  27970  pntibnd  27977  pntlem3  27993  pntleml  27995  fltoprm  28052  ltsres  28076  nosepon  28079  nolesgn2o  28085  nogesgn1o  28087  nodenselem8  28105  nosupbnd1lem1  28122  madess  28309  madebdaylemlrcut  28342  peano5uzs  28847  bdayfinbndlem1  28910  z12bday  28928  brbtwn2  29540  colinearalg  29545  axcontlem10  29608  edgupgr  29769  edglnl  29778  usgruspgrb  29821  subupgr  29925  uhgrspan1  29941  usgredgsscusgredg  30097  fusgrn0degnn0  30137  upgrewlkle2  30244  uspgr2wlkeq  30283  redwlk  30308  wlkdlem2  30319  upgrwlkdvdelem  30379  pthdlem1  30409  pthdlem2  30411  crctcshwlkn0lem3  30458  wlkiswwlks1  30513  wwlksm1edg  30527  wwlksnred  30538  wwlksnextbi  30540  umgr2adedgspth  30594  clwlkclwwlklem2fv2  30644  clwlkclwwlklem2a  30646  clwlkclwwlkf1lem3  30654  clwwisshclwwslemlem  30661  clwwlkf  30695  clwwlkext2edg  30704  wwlksubclwwlk  30706  clwwlknonex2lem2  30756  loop1cycl  30801  eupth2lems  30896  frgrwopreglem4a  30968  frgrregorufrg  30984  ex-natded5.3-2  31066  isgrpo  31156  vacn  31353  ubthlem2  31530  htthlem  31576  normgt0  31786  shmodsi  32048  spansneleq  32229  h1datomi  32240  nmcexi  32685  pjnormssi  32827  stm1add3i  32906  golem2  32931  cvnsym  32949  dmdmd  32959  mdslmd1lem1  32984  mdslmd1i  32988  mdexchi  32994  atcveq0  33007  superpos  33013  hatomistici  33021  atoml2i  33042  atcvat2i  33046  chirredlem1  33049  atcvat3i  33055  mdsymlem3  33064  mdsymlem5  33066  cdj3lem2b  33096  cdj3i  33100  submarchi  33846  dfufd2  34186  tpr2rico  34655  ordtrest2NEWlem  34665  xrge0iifcnv  34676  omssubadd  35043  eulerpartlemb  35111  ballotlemfc0  35236  ballotlemfcc  35237  ftc2re  35338  fineqvinfep  35934  axsepg2  35949  axsepg4  35952  axpowg2  35956  axpowg3  35957  j0ltaleph  36049  subfacp1lem6  36158  iccllysconn  36223  cvmfolem  36252  satfsschain  36337  satfrel  36340  satfdm  36342  sat1el2xp  36352  satffunlem1lem1  36375  dmopab3rexdif  36378  satffunlem2lem2  36379  satffun  36382  mirimanofffr  36670  fundmpss  36747  dfon2lem3  36762  dfon2lem6  36765  axextbdist  36777  dfrdg4  36930  5segofs  36986  cgrextend  36988  segconeu  36991  btwncomim  36993  btwnswapid  36997  btwnintr  36999  btwnexch3  37000  btwndiff  37007  ifscgr  37024  cgrxfr  37035  btwnxfr  37036  lineext  37056  brofs2  37057  linecgr  37061  lineid  37063  idinside  37064  endofsegid  37065  btwnconn1lem13  37079  btwnconn3  37083  finminlem  37321  nn0prpwlem  37325  cldbnd  37329  clsint2  37332  fnessref  37360  neibastop3  37365  fgmin  37373  onsuct0  37444  limsucncmpi  37448  tr0elw  37487  tr0el  37488  bj-nnfea  37851  bj-axc14  37983  bj-restn0  38281  bj-0int  38292  wl-19.2reqv  38724  wl-aetr  38729  wl-axc11r  38730  fin2so  38798  tan2h  38803  poimirlem2  38808  poimirlem9  38815  poimirlem17  38823  poimirlem18  38824  poimirlem21  38827  poimirlem23  38829  poimirlem26  38832  poimirlem29  38835  poimirlem30  38836  poimirlem31  38837  poimir  38839  heicant  38841  mblfinlem2  38844  mblfinlem3  38845  itg2addnclem  38857  itg2addnclem2  38858  itg2gt0cn  38861  ftc1anclem5  38883  ftc1anclem6  38884  findcard4  38900  dfprop2  38914  filbcmb  38940  nninfnub  38951  mettrifi  38957  geomcau  38959  istotbnd3  38971  sstotbnd2  38974  ismtybndlem  39006  heibor1lem  39009  heiborlem1  39011  heiborlem8  39018  heiborlem10  39020  heibor  39021  opidonOLD  39052  riscer  39188  crngohomfo  39206  keridl  39232  ispridl2  39238  ispridlc  39270  ac6s6  39370  eqvreltr  39889  eldisjdmqsim  40015  suceldisj  40016  eldisjs6  40138  dral1-o  40227  ax12indalem  40268  ax12inda2ALT  40269  lsatcveq0  40355  eqlkr3  40424  atlatmstc  40642  atlrelat1  40644  hlrelat2  40726  intnatN  40730  cvrexchlem  40742  cvratlem  40744  cvrat2  40752  atltcvr  40758  cvrat3  40765  cvrat4  40766  ps-1  40800  ps-2  40801  lplnnle2at  40864  lvolnle3at  40905  2llnma3r  41111  cdlemblem  41116  pmapjoin  41175  elpcliN  41216  lhpmcvr4N  41349  4atexlemnclw  41393  trlnidatb  41500  cdlemc4  41517  cdlemd3  41523  cdleme3g  41557  cdleme7d  41569  cdleme11c  41584  cdleme11dN  41585  cdleme21b  41649  cdleme21c  41650  cdleme21i  41658  cdleme22b  41664  cdleme35fnpq  41772  cdlemf1  41884  trlord  41892  cdlemg6c  41943  dihglblem6  42663  dochlkr  42708  dochkrshp  42709  dihjat1lem  42751  dochexmidlem5  42787  dochexmidlem8  42790  qsalrel  43559  remulcand  43756  fphpdo  44090  pellexlem5  44106  pellexlem6  44107  jm2.26lem3  44274  unxpwdom3  44363  omlimcl2  44505  oe0suclim  44540  cantnfresb  44587  tfsconcatb0  44607  naddgeoa  44657  iscard5  44798  sqrtcval  44902  ov2ssiunov2  44961  frege124d  45022  19.41rg  45793  relpfrlem  46207  modelaxreplem2  46233  stoweidlem34  47317  ormklocald  48159  evenwodadd  48184  cfsetsnfsetf1  48402  fcoresf1  48412  euoreqb  48453  2reu8i  48457  ralralimp  48621  f1oresf1o2  48634  zm1nn  48645  elfz2z  48658  2tceilhalfelfzo1  48679  m1modmmod  48707  modlt0b  48712  muldvdsfacgt  48729  muldvdsfacm1  48730  iccpartlt  48779  iccelpart  48788  icceuelpartlem  48790  fargshiftf1  48796  sprsymrelf1lem  48846  paireqne  48866  reuopreuprim  48881  goldbachthlem2  48904  odz2prm2pw  48921  fmtnoprmfac1lem  48922  fmtnofac2lem  48926  prmdvdsfmtnof1  48945  sfprmdvdsmersenne  48961  lighneallem2  48964  lighneallem4  48968  fppr2odd  49102  gbegt5  49132  gbowge7  49134  bgoldbtbndlem4  49179  bgoldbtbnd  49180  tgoldbach  49188  grimuhgr  49258  grimcnv  49259  grimco  49260  isuspgrim0  49265  isuspgrimlem  49266  upgrimwlklem5  49272  upgrimtrlslem2  49276  uhgrimisgrgriclem  49301  clnbgrgrimlem  49304  clnbgrgrim  49305  grimedg  49306  grtriprop  49312  isubgr3stgrlem3  49339  isubgr3stgrlem4  49340  isubgr3stgrlem6  49342  isubgr3stgrlem7  49343  uspgrlimlem3  49361  grlimedgclnbgr  49366  grlimgrtrilem2  49373  grlimgrtri  49374  grlicsym  49384  gpgedgvtx1  49433  gpgedgiov  49436  gpgedg2ov  49437  gpgedg2iv  49438  pgnioedg1  49479  pgnioedg2  49480  pgnioedg3  49481  pgnioedg4  49482  pgnioedg5  49483  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  pgnbgreunbgrlem5lem1  49491  pgnbgreunbgrlem5lem2  49492  pgnbgreunbgrlem5lem3  49493  lazssaz  49730  lazmulzcl  49737  lazmulcl  49740  lazcjcl  49741  lcosslsp  49881  lindslinindsimp1  49900  snlindsntor  49914  itcovalt2  50120  eenglngeehlnmlem2  50182  itsclc0yqsol  50207  itschlc0xyqsol1  50209  itschlc0xyqsol  50210  opnneilv  50354  i0oii  50365  io1ii  50366  iscnrm3lem4  50381  iscnrm3r  50393  aacllem  51367