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  2248  sylan9eq  2285  csbcomg  3160  sylan9ss  3250  ssconb  3351  ineqan12d  3423  dfopg  3880  breqan12d  4124  opexg  4343  copsex2g  4361  ordin  4505  onin  4506  unexg  4563  eusv1  4572  opelvvg  4798  opthprc  4800  opbrop  4828  relop  4904  dmpropg  5234  unixpm  5297  funssres  5394  funinsn  5404  funtp  5408  fnco  5465  resasplitss  5543  fodmrnu  5597  relrnfvex  5687  funopdmsn  5863  fconst2g  5898  oveqan12d  6068  ovi3  6190  ovg  6192  f1opw2  6260  off  6278  offres  6327  suppfnss  6456  iunon  6514  nnsucsssuc  6724  nnaword1  6745  ertr  6781  erex  6790  brecop  6858  ecovdi  6879  ecovidi  6880  mapvalg  6891  pmvalg  6892  pmss12g  6908  mapsn  6924  en2sn  7054  xpf1o  7096  xpen  7097  phplem4  7108  ssfilem  7129  ssfilemd  7131  diffitest  7143  en1eqsn  7217  sbthlem7  7232  fsuppxpfi  7248  ordiso  7326  updjud  7372  fodju0  7437  finnum  7478  pr2nelem  7487  djucomen  7522  exmidontriimlem1  7527  2onetap  7565  ltsopi  7631  pitric  7632  pitri3or  7633  ltdcpi  7634  mulclpi  7639  addcompig  7640  mulcompig  7642  distrpig  7644  ltexpi  7648  ltapig  7649  ltmpig  7650  dfplpq2  7665  dfmpq2  7666  enqbreq2  7668  enqdc  7672  addcmpblnq  7678  addpipqqslem  7680  mulpipq2  7682  mulpipq  7683  mulpipqqs  7684  addclnq  7686  distrnqg  7698  ltdcnq  7708  ltrnqg  7731  enq0breq  7747  addclnq0  7762  nqnq0a  7765  nqnq0m  7766  nq0m0r  7767  distrnq0  7770  mulcomnq0  7771  genipv  7820  genplt2i  7821  genpelvl  7823  genpelvu  7824  addnqprlemrl  7868  addnqprlemru  7869  addnqprlemfl  7870  addnqprlemfu  7871  addnqpr  7872  mulnqprlemrl  7884  mulnqprlemru  7885  mulnqprlemfl  7886  mulnqprlemfu  7887  mulnqpr  7888  distrlem4prl  7895  distrlem4pru  7896  ltnqpr  7904  recexprlemloc  7942  archrecnq  7974  mulclsr  8065  1idsr  8079  00sr  8080  prsradd  8097  axmulass  8184  axdistr  8185  axcnre  8192  peano5nnnn  8203  mulrid  8267  axltadd  8339  lenlt  8345  cnegexlem3  8446  cnegex  8447  resubcl  8533  subeqrev  8645  muladd  8653  mulsub  8670  mulsub2  8671  ltaddsub2  8707  leaddsub2  8709  leltadd  8717  ltaddpos2  8723  posdif  8725  addge02  8743  mullt0  8750  recexre  8848  recextlem1  8921  recexap  8923  divmuldivap  8982  conjmulap  8999  div2subap  9107  prodgt02  9123  prodge02  9125  lemul2  9127  lemul2a  9129  ltmulgt12  9135  lemulge12  9137  ltmuldiv2  9145  ltdivmul2  9148  ledivmul2  9150  lemuldiv2  9152  negiso  9225  cju  9231  peano5nni  9236  nnaddcl  9253  nnmulcl  9254  nnsub  9272  addltmul  9471  avgle1  9475  avgle2  9476  nnrecl  9490  nn0nnaddcl  9523  zsubcl  9614  zleloe  9620  znnsub  9625  nzadd  9626  zmulcl  9627  zltp1le  9628  zleltp1  9629  nnleltp1  9633  nnltp1le  9634  nnaddm1cl  9635  nn0ltp1le  9636  nn0leltp1  9637  nn0ltlem1  9638  znn0sub  9639  nn0sub  9640  elz2  9645  zapne  9648  zdcle  9650  zdclt  9651  zltlen  9652  nn0lem1lt  9657  nnlem1lt  9658  nnltlem1  9659  zdiv  9662  zextle  9665  zextlt  9666  btwnnz  9668  prime  9673  nneo  9677  peano2uz2  9681  peano5uzti  9682  uzind  9685  fzind  9689  fnn0ind  9690  uzneg  9869  uz11  9873  eluzp1m1  9874  eluzp1p1  9876  uzin  9883  indstr  9921  uz2mulcl  9936  qre  9953  qaddcl  9963  qsubcl  9966  qltlen  9968  qlttri2  9969  irradd  9974  elpqb  9978  cnref1o  9979  rpaddcl  10006  rpmulcl  10007  rpdivcl  10008  rexadd  10181  rexsub  10182  xaddcom  10190  xnn0xadd0  10196  xnegdi  10197  elicc2  10267  iccshftr  10323  iccshftl  10325  iccdil  10327  icccntr  10329  fzval2  10341  elfz1eq  10365  peano2fzr  10367  fznlem  10371  fzsplit2  10380  fzaddel  10389  fzsubel  10390  fzrev2  10415  fzrev3  10417  uzsplit  10422  fzrevral  10435  fzrevral3  10437  fzshftral  10438  elfz2nn0  10442  fznn0sub2  10458  fz0fzdiffz0  10460  elfzmlbp  10462  difelfzle  10464  difelfznle  10465  1fv  10469  elfzouz2  10492  fzo0n  10498  fzouzsplit  10511  fzoun  10513  elfzo0le  10520  fzonmapblen  10522  fzofzim  10523  fzoaddel2  10531  eluzgtdifelfzo  10538  elfzodifsumelfzo  10542  ubmelm1fzo  10567  fzofzp1b  10569  fzosplitprm1  10576  fzostep1  10579  subfzo0  10584  zsupcllemstep  10585  qdclt  10601  qbtwnxr  10613  flqbi2  10647  divfl0  10652  flqzadd  10654  flqmulnn0  10655  addmodidr  10731  modfzo0difsn  10753  frec2uzltd  10761  frec2uzrand  10763  frecfzen2  10785  seqshft2g  10840  seq3split  10846  seqsplitg  10847  seq3caopr2  10851  seqcaopr2g  10852  seqf1oglem2  10878  exp3vallem  10898  expcllem  10908  expcl2lemap  10909  1exp  10926  expge1  10934  expadd  10939  expmul  10942  expsubap  10945  leexp1a  10952  lt2sq  10971  le2sq  10972  sumsqeq0  10976  qsqeqor  11008  bernneq  11018  bernneq2  11019  sq11ap  11065  facdiv  11096  faclbnd  11099  faclbnd3  11101  faclbnd6  11102  facavg  11104  bcrpcl  11111  bccmpl  11112  fiubm  11188  seq3coll  11207  eqwrd  11258  ccatcl  11274  ccatclab  11275  ccatlen  11276  ccat0  11277  ccatval1  11278  ccatval2  11279  elfzelfzccat  11281  ccatvalfn  11282  ccatsymb  11283  ccatval21sw  11286  ccatrn  11290  lswccatn0lsw  11292  ccatalpha  11294  ccatrcl1  11295  swrdfv2  11348  swrdsbslen  11351  swrdspsleq  11352  swrdccat2  11356  pfxclz  11364  ccatpfx  11386  pfxccat1  11387  swrdswrdlem  11389  pfxswrd  11391  pfxccatin12lem4  11411  pfxccatin12lem1  11413  pfxccatin12lem2  11416  pfxccatin12lem3  11417  pfxccat3  11419  swrdccat  11420  pfxccatpfx2  11422  pfxccat3a  11423  swrdccat3blem  11424  swrdccat3b  11425  s2dmg  11475  shftfvalg  11496  shftf  11508  crre  11535  crim  11536  mulreap  11542  readd  11547  resub  11548  remul2  11551  imadd  11555  imsub  11556  immul2  11558  ipcnval  11564  cjsub  11570  cjreim  11581  caucvgre  11659  rexanuz  11666  rexuz3  11668  resqrexlemover  11688  resqrexlemcvg  11697  resqrexlemglsq  11700  sqrtle  11714  sqrtlt  11715  sqrt11ap  11716  sqrt11  11717  absreimsq  11745  absreim  11746  absmul  11747  sqabs  11760  absdiflt  11770  absdifle  11771  abssuble0  11781  abs2difabs  11786  fzomaxdif  11791  caubnd2  11795  rpmaxcl  11901  zmaxcl  11902  nn0maxcl  11903  minmax  11908  mincl  11909  min1inf  11910  min2inf  11911  minabs  11914  minclpr  11915  rpmincl  11916  2zinfmin  11921  xrmaxrecl  11933  xrminmax  11943  xrmincl  11944  xrmin1inf  11945  xrmin2inf  11946  xrminrecl  11951  xrminrpcl  11952  iooinsup  11955  climconst2  11969  climuni  11971  2clim  11979  climshft  11982  climshft2  11984  cjcn2  11994  climaddc1  12007  climmulc2  12009  climsubc1  12010  climsubc2  12011  climlec2  12019  summodclem2a  12060  zsumdc  12063  isumclim3  12102  mptfzshft  12121  fsumrev  12122  fisum0diag2  12126  telfsumo2  12146  fsumparts  12149  cvgcmpub  12155  binomlem  12162  binom1p  12164  binom1dif  12166  bcxmas  12168  isumshft  12169  expcnvap0  12181  expcnv  12183  geosergap  12185  geolim  12190  cvgratnnlemrate  12209  mertenslemi1  12214  mertenslem2  12215  mertensabs  12216  prodmodc  12257  zproddc  12258  fprodf1o  12267  fprodeq0  12296  efcj  12352  eftlub  12369  effsumlt  12371  efieq  12414  sinsub  12419  cossub  12420  subsin  12422  sinmul  12423  cosmul  12424  addcos  12425  subcos  12426  dvdssub2  12514  dvdsadd  12515  dvdsaddr  12516  dvdssub  12517  dvdssubr  12518  fzocongeq  12537  odd2np1  12552  opoe  12574  omoe  12575  opeo  12576  omeo  12577  divalgb  12604  ndvdsadd  12610  bitsfi  12636  gcdmndc  12644  gcdabs  12677  dvdsgcd  12701  absmulgcd  12706  gcdmultiple  12709  gcdmultiplez  12710  rpmulgcd  12715  sqgcd  12718  dvdssqlem  12719  dvdssq  12720  nninfctlemfo  12729  nn0seqcvgd  12731  ialgrlemconst  12733  algrf  12735  algrp1  12736  algcvg  12738  algcvga  12741  lcmval  12753  lcmabs  12766  lcmgcd  12768  lcmdvds  12769  lcmgcdnn  12772  coprmgcdb  12778  coprmdvds  12782  coprmdvds2  12783  qredeq  12786  isprm3  12808  nprm  12813  divgcdodd  12833  prmdvdsexp  12838  sqrt2irr  12852  zgcdsq  12891  hashdvds  12911  phiprmpw  12912  crth  12914  phimullem  12915  modprm0  12945  coprimeprodsq  12948  coprimeprodsq2  12949  pythagtriplem2  12957  pythagtriplem19  12973  pcdvdsb  13011  pcneg  13016  pc2dvds  13021  pc11  13022  pcmpt  13034  pcfac  13041  infpnlem1  13050  prmunb  13053  1arithlem4  13057  1arith  13058  gzaddcl  13068  gzmulcl  13069  gzreim  13070  gzsubcl  13071  4sqlem1  13079  4sqlem4a  13082  4sqlem4  13083  4sqlem12  13093  setsvalg  13231  setsfun0  13237  restval  13447  xpsval  13554  mndinvmod  13647  resmhm  13689  resmhm2  13690  mhmco  13692  dfgrp3m  13801  mhmmnd  13822  mulgnngsum  13833  mulgnn0z  13855  mulgnndir  13857  ghmex  13961  0ghm  13964  resghm  13966  resghm2  13967  ghmco  13970  ghmeql  13973  kerf1ghm  13980  ablsubsub23  14031  dfrhm2  14288  isrhm  14292  rhmfn  14306  rhmval  14307  rhmco  14308  resrhm  14382  rhmeql  14384  rhmima  14385  lmodfopne  14461  lspf  14524  znidom  14792  znrrg  14795  innei  15015  cnovex  15048  txuni2  15108  txbasex  15109  txbas  15110  txtop  15112  txtopon  15114  txss12  15118  txbasval  15119  txcnp  15123  upxp  15124  txcnmpt  15125  uptx  15126  txcn  15127  txrest  15128  txdis  15129  cnmpt21  15143  hmeoco  15168  txhmeo  15171  isxmet2d  15200  blin2  15284  comet  15351  metcn  15366  txmetcn  15371  qtopbasss  15373  qtopbas  15374  remetdval  15399  bl2ioo  15402  blssioo  15405  divcnap  15417  cncfmet  15444  dvaddxxbr  15553  dvcjbr  15560  plyf  15589  ply1termlem  15594  plymullem1  15600  plyaddlem  15601  plymullem  15602  plycolemc  15610  plyreres  15616  dvply1  15617  efle  15628  reapef  15630  sinperlem  15660  sincosq2sgn  15679  sincosq3sgn  15680  sincos6thpi  15694  ioocosf1o  15706  relogoprlem  15720  logleb  15727  cxple3  15773  cxpcom  15790  dvdsppwf1o  15844  fsumdvdsmul  15846  1sgmprm  15849  mersenne  15852  lgslem3  15862  lgsdir2  15893  lgsdir  15895  lgsdilem2  15896  lgsdi  15897  gausslemma2dlem1a  15918  gausslemma2dlem3  15923  gausslemma2dlem6  15927  lgseisenlem3  15932  lgseisenlem4  15933  lgsquadlem1  15937  lgsquadlem2  15938  lgsquad2  15943  lgsquad3  15944  2lgslem1a1  15946  2lgslem1a  15948  2lgslem1c  15950  2sqlem2  15975  mul2sq  15976  2sqlem7  15981  usgredg2v  16206  ushgredgedg  16208  ushgredgedgloop  16210  uhgrissubgr  16243  vtxedgfi  16271  vtxlpfi  16272  wlkeq  16336  uspgr2wlkeq  16347  clwwlkccatlem  16382  clwwlkccat  16383  clwwlknccat  16405  bj-inex  16664  bj-bdfindis  16704  triap  16800  cvgcmp2nlemabs  16803  trilpolemisumle  16809  inffz  16844