Theorem syl2an 289

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2an	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 ⊢ (𝜏 → 𝜒)
2		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 283	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2 286	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  syl2anr  290  anim12i  338  syl2an2  598  syl2an2r  599  orandc  948  mp3an3an  1380  eqeqan12d  2250  sylan9eq  2287  csbcomg  3163  sylan9ss  3253  ssconb  3354  ineqan12d  3426  dfopg  3883  breqan12d  4127  opexg  4346  copsex2g  4364  ordin  4508  onin  4509  unexg  4566  eusv1  4575  opelvvg  4801  opthprc  4803  opbrop  4831  relop  4907  dmpropg  5237  unixpm  5300  funssres  5397  funinsn  5407  funtp  5411  fnco  5468  resasplitss  5546  fodmrnu  5600  relrnfvex  5690  funopdmsn  5866  fconst2g  5901  oveqan12d  6071  ovi3  6193  ovg  6195  f1opw2  6263  off  6281  offres  6330  suppfnss  6459  iunon  6517  nnsucsssuc  6727  nnaword1  6748  ertr  6784  erex  6793  brecop  6861  ecovdi  6882  ecovidi  6883  mapvalg  6894  pmvalg  6895  pmss12g  6911  mapsn  6927  en2sn  7057  xpf1o  7099  xpen  7100  phplem4  7111  ssfilem  7132  ssfilemd  7134  diffitest  7146  en1eqsn  7220  sbthlem7  7235  fsuppxpfi  7251  ordiso  7329  updjud  7375  fodju0  7440  finnum  7481  pr2nelem  7490  djucomen  7525  exmidontriimlem1  7530  2onetap  7574  ltsopi  7640  pitric  7641  pitri3or  7642  ltdcpi  7643  mulclpi  7648  addcompig  7649  mulcompig  7651  distrpig  7653  ltexpi  7657  ltapig  7658  ltmpig  7659  dfplpq2  7674  dfmpq2  7675  enqbreq2  7677  enqdc  7681  addcmpblnq  7687  addpipqqslem  7689  mulpipq2  7691  mulpipq  7692  mulpipqqs  7693  addclnq  7695  distrnqg  7707  ltdcnq  7717  ltrnqg  7740  enq0breq  7756  addclnq0  7771  nqnq0a  7774  nqnq0m  7775  nq0m0r  7776  distrnq0  7779  mulcomnq0  7780  genipv  7829  genplt2i  7830  genpelvl  7832  genpelvu  7833  addnqprlemrl  7877  addnqprlemru  7878  addnqprlemfl  7879  addnqprlemfu  7880  addnqpr  7881  mulnqprlemrl  7893  mulnqprlemru  7894  mulnqprlemfl  7895  mulnqprlemfu  7896  mulnqpr  7897  distrlem4prl  7904  distrlem4pru  7905  ltnqpr  7913  recexprlemloc  7951  archrecnq  7983  mulclsr  8074  1idsr  8088  00sr  8089  prsradd  8106  axmulass  8193  axdistr  8194  axcnre  8201  peano5nnnn  8212  mulrid  8276  axltadd  8348  lenlt  8354  cnegexlem3  8455  cnegex  8456  resubcl  8542  subeqrev  8654  muladd  8662  mulsub  8679  mulsub2  8680  ltaddsub2  8716  leaddsub2  8718  leltadd  8726  ltaddpos2  8732  posdif  8734  addge02  8752  mullt0  8759  recexre  8857  recextlem1  8930  recexap  8932  divmuldivap  8991  conjmulap  9008  div2subap  9116  prodgt02  9132  prodge02  9134  lemul2  9136  lemul2a  9138  ltmulgt12  9144  lemulge12  9146  ltmuldiv2  9154  ltdivmul2  9157  ledivmul2  9159  lemuldiv2  9161  negiso  9234  cju  9240  peano5nni  9245  nnaddcl  9262  nnmulcl  9263  nnsub  9281  addltmul  9480  avgle1  9484  avgle2  9485  nnrecl  9499  nn0nnaddcl  9532  zsubcl  9623  zleloe  9629  znnsub  9634  nzadd  9635  zmulcl  9636  zltp1le  9637  zleltp1  9638  nnleltp1  9642  nnltp1le  9643  nnaddm1cl  9644  nn0ltp1le  9645  nn0leltp1  9646  nn0ltlem1  9647  znn0sub  9648  nn0sub  9649  elz2  9654  zapne  9657  zdcle  9659  zdclt  9660  zltlen  9662  nn0lem1lt  9667  nnlem1lt  9668  nnltlem1  9669  zdiv  9672  zextle  9675  zextlt  9676  btwnnz  9678  prime  9683  nneo  9687  peano2uz2  9691  peano5uzti  9692  uzind  9695  fzind  9699  fnn0ind  9700  uzneg  9879  uz11  9883  eluzp1m1  9884  eluzp1p1  9886  uzin  9893  indstr  9931  uz2mulcl  9946  qre  9963  qaddcl  9973  qsubcl  9976  qltlen  9978  qlttri2  9979  irradd  9984  elpqb  9988  cnref1o  9989  rpaddcl  10016  rpmulcl  10017  rpdivcl  10018  rexadd  10191  rexsub  10192  xaddcom  10200  xnn0xadd0  10206  xnegdi  10207  elicc2  10277  iccshftr  10333  iccshftl  10335  iccdil  10337  icccntr  10339  fzval2  10351  elfz1eq  10375  peano2fzr  10377  fznlem  10381  fzsplit2  10390  fzaddel  10399  fzsubel  10400  fzrev2  10426  fzrev3  10428  uzsplit  10433  fzrevral  10446  fzrevral3  10448  fzshftral  10449  elfz2nn0  10453  fznn0sub2  10469  fz0fzdiffz0  10471  elfzmlbp  10473  difelfzle  10475  difelfznle  10476  1fv  10480  elfzouz2  10503  fzo0n  10509  fzouzsplit  10522  fzoun  10524  elfzo0le  10531  fzonmapblen  10533  fzofzim  10534  fzoaddel2  10542  eluzgtdifelfzo  10549  elfzodifsumelfzo  10553  ubmelm1fzo  10578  fzofzp1b  10580  fzosplitprm1  10587  fzostep1  10590  subfzo0  10595  zsupcllemstep  10596  qdclt  10612  qbtwnxr  10624  flqbi2  10658  divfl0  10663  flqzadd  10665  flqmulnn0  10666  addmodidr  10742  modfzo0difsn  10764  frec2uzltd  10772  frec2uzrand  10774  frecfzen2  10796  seqshft2g  10851  seq3split  10857  seqsplitg  10858  seq3caopr2  10862  seqcaopr2g  10863  seqf1oglem2  10889  exp3vallem  10909  expcllem  10919  expcl2lemap  10920  1exp  10937  expge1  10945  expadd  10950  expmul  10953  expsubap  10956  leexp1a  10963  lt2sq  10982  le2sq  10983  sumsqeq0  10987  qsqeqor  11019  bernneq  11030  bernneq2  11031  sq11ap  11077  facdiv  11108  faclbnd  11111  faclbnd3  11113  faclbnd6  11114  facavg  11116  bcrpcl  11123  bccmpl  11124  bcm1n  11139  fiubm  11203  seq3coll  11222  eqwrd  11273  ccatcl  11289  ccatclab  11290  ccatlen  11291  ccat0  11292  ccatval1  11293  ccatval2  11294  elfzelfzccat  11296  ccatvalfn  11297  ccatsymb  11298  ccatval21sw  11301  ccatrn  11305  lswccatn0lsw  11307  ccatalpha  11309  ccatrcl1  11310  swrdfv2  11363  swrdsbslen  11366  swrdspsleq  11367  swrdccat2  11371  pfxclz  11379  ccatpfx  11401  pfxccat1  11402  swrdswrdlem  11404  pfxswrd  11406  pfxccatin12lem4  11426  pfxccatin12lem1  11428  pfxccatin12lem2  11431  pfxccatin12lem3  11432  pfxccat3  11434  swrdccat  11435  pfxccatpfx2  11437  pfxccat3a  11438  swrdccat3blem  11439  swrdccat3b  11440  s2dmg  11490  shftfvalg  11511  shftf  11523  crre  11550  crim  11551  mulreap  11557  readd  11562  resub  11563  remul2  11566  imadd  11570  imsub  11571  immul2  11573  ipcnval  11579  cjsub  11585  cjreim  11596  caucvgre  11674  rexanuz  11681  rexuz3  11683  resqrexlemover  11703  resqrexlemcvg  11712  resqrexlemglsq  11715  sqrtle  11729  sqrtlt  11730  sqrt11ap  11731  sqrt11  11732  absreimsq  11760  absreim  11761  absmul  11762  sqabs  11775  absdiflt  11785  absdifle  11786  abssuble0  11796  abs2difabs  11801  fzomaxdif  11806  caubnd2  11810  rpmaxcl  11916  zmaxcl  11917  nn0maxcl  11918  minmax  11923  mincl  11924  min1inf  11925  min2inf  11926  minabs  11929  minclpr  11930  rpmincl  11931  2zinfmin  11936  xrmaxrecl  11948  xrminmax  11958  xrmincl  11959  xrmin1inf  11960  xrmin2inf  11961  xrminrecl  11966  xrminrpcl  11967  iooinsup  11970  climconst2  11984  climuni  11986  2clim  11994  climshft  11997  climshft2  11999  cjcn2  12009  climaddc1  12022  climmulc2  12024  climsubc1  12025  climsubc2  12026  climlec2  12034  summodclem2a  12075  zsumdc  12078  isumclim3  12117  mptfzshft  12136  fsumrev  12137  fisum0diag2  12141  telfsumo2  12161  fsumparts  12164  cvgcmpub  12170  binomlem  12177  binom1p  12179  binom1dif  12181  bcxmas  12183  isumshft  12184  expcnvap0  12196  expcnv  12198  geosergap  12200  geolim  12205  cvgratnnlemrate  12224  mertenslemi1  12229  mertenslem2  12230  mertensabs  12231  prodmodc  12272  zproddc  12273  fprodf1o  12282  fprodeq0  12311  efcj  12367  eftlub  12384  effsumlt  12386  efieq  12429  sinsub  12434  cossub  12435  subsin  12437  sinmul  12438  cosmul  12439  addcos  12440  subcos  12441  dvdssub2  12529  dvdsadd  12530  dvdsaddr  12531  dvdssub  12532  dvdssubr  12533  fzocongeq  12552  odd2np1  12567  opoe  12589  omoe  12590  opeo  12591  omeo  12592  divalgb  12619  ndvdsadd  12625  bitsfi  12651  gcdmndc  12659  gcdabs  12692  dvdsgcd  12716  absmulgcd  12721  gcdmultiple  12724  gcdmultiplez  12725  rpmulgcd  12730  sqgcd  12733  dvdssqlem  12734  dvdssq  12735  nninfctlemfo  12744  nn0seqcvgd  12746  ialgrlemconst  12748  algrf  12750  algrp1  12751  algcvg  12753  algcvga  12756  lcmval  12768  lcmabs  12781  lcmgcd  12783  lcmdvds  12784  lcmgcdnn  12787  coprmgcdb  12793  coprmdvds  12797  coprmdvds2  12798  qredeq  12801  isprm3  12823  nprm  12828  divgcdodd  12848  prmdvdsexp  12853  sqrt2irr  12867  zgcdsq  12906  hashdvds  12926  phiprmpw  12927  crth  12929  phimullem  12930  modprm0  12960  coprimeprodsq  12963  coprimeprodsq2  12964  pythagtriplem2  12972  pythagtriplem19  12988  pcdvdsb  13026  pcneg  13031  pc2dvds  13036  pc11  13037  pcmpt  13049  pcfac  13056  infpnlem1  13065  prmunb  13068  1arithlem4  13072  1arith  13073  gzaddcl  13083  gzmulcl  13084  gzreim  13085  gzsubcl  13086  4sqlem1  13094  4sqlem4a  13097  4sqlem4  13098  4sqlem12  13108  ballotfilemfc0  13157  ballotfilemfcc  13158  setsvalg  13263  setsfun0  13269  restval  13479  xpsval  13586  mndinvmod  13679  resmhm  13721  resmhm2  13722  mhmco  13724  dfgrp3m  13833  mhmmnd  13854  mulgnngsum  13865  mulgnn0z  13887  mulgnndir  13889  ghmex  13993  0ghm  13996  resghm  13998  resghm2  13999  ghmco  14002  ghmeql  14005  kerf1ghm  14012  ablsubsub23  14063  dfrhm2  14321  isrhm  14325  rhmfn  14339  rhmval  14340  rhmco  14341  resrhm  14416  rhmeql  14418  rhmima  14419  lmodfopne  14523  lspf  14586  znidom  14854  znrrg  14857  innei  15077  cnovex  15110  txuni2  15170  txbasex  15171  txbas  15172  txtop  15174  txtopon  15176  txss12  15180  txbasval  15181  txcnp  15185  upxp  15186  txcnmpt  15187  uptx  15188  txcn  15189  txrest  15190  txdis  15191  cnmpt21  15205  hmeoco  15230  txhmeo  15233  isxmet2d  15262  blin2  15346  comet  15413  metcn  15428  txmetcn  15433  qtopbasss  15435  qtopbas  15436  remetdval  15461  bl2ioo  15464  blssioo  15467  divcnap  15479  cncfmet  15506  dvaddxxbr  15615  dvcjbr  15622  plyf  15651  ply1termlem  15656  plymullem1  15662  plyaddlem  15663  plymullem  15664  plycolemc  15672  plyreres  15678  dvply1  15679  efle  15690  reapef  15692  sinperlem  15722  sincosq2sgn  15741  sincosq3sgn  15742  sincos6thpi  15756  ioocosf1o  15768  relogoprlem  15782  logleb  15789  cxple3  15835  cxpcom  15852  dvdsppwf1o  15906  fsumdvdsmul  15908  1sgmprm  15911  mersenne  15914  lgslem3  15924  lgsdir2  15955  lgsdir  15957  lgsdilem2  15958  lgsdi  15959  gausslemma2dlem1a  15980  gausslemma2dlem3  15985  gausslemma2dlem6  15989  lgseisenlem3  15994  lgseisenlem4  15995  lgsquadlem1  15999  lgsquadlem2  16000  lgsquad2  16005  lgsquad3  16006  2lgslem1a1  16008  2lgslem1a  16010  2lgslem1c  16012  2sqlem2  16037  mul2sq  16038  2sqlem7  16043  usgredg2v  16268  ushgredgedg  16270  ushgredgedgloop  16272  uhgrissubgr  16305  vtxedgfi  16333  vtxlpfi  16334  wlkeq  16398  uspgr2wlkeq  16409  clwwlkccatlem  16444  clwwlkccat  16445  clwwlknccat  16467  bj-inex  16726  bj-bdfindis  16766  triap  16862  cvgcmp2nlemabs  16865  trilpolemisumle  16871  inffz  16907