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  596  syl2an2r  597  orandc  945  mp3an3an  1377  eqeqan12d  2245  sylan9eq  2282  csbcomg  3147  sylan9ss  3237  ssconb  3337  ineqan12d  3407  dfopg  3854  breqan12d  4098  opexg  4313  copsex2g  4331  ordin  4475  onin  4476  unexg  4533  eusv1  4542  opelvvg  4767  opthprc  4769  opbrop  4797  relop  4871  dmpropg  5200  unixpm  5263  funssres  5359  funinsn  5369  funtp  5373  fnco  5430  resasplitss  5504  fodmrnu  5555  relrnfvex  5644  funopdmsn  5818  fconst2g  5853  oveqan12d  6019  ovi3  6141  ovg  6143  f1opw2  6210  off  6229  offres  6278  iunon  6428  nnsucsssuc  6636  nnaword1  6657  ertr  6693  erex  6702  brecop  6770  ecovdi  6791  ecovidi  6792  mapvalg  6803  pmvalg  6804  pmss12g  6820  mapsn  6835  en2sn  6964  xpf1o  7001  xpen  7002  phplem4  7012  ssfilem  7033  diffitest  7045  en1eqsn  7111  sbthlem7  7126  ordiso  7199  updjud  7245  fodju0  7310  finnum  7351  pr2nelem  7360  djucomen  7394  exmidontriimlem1  7399  2onetap  7437  ltsopi  7503  pitric  7504  pitri3or  7505  ltdcpi  7506  mulclpi  7511  addcompig  7512  mulcompig  7514  distrpig  7516  ltexpi  7520  ltapig  7521  ltmpig  7522  dfplpq2  7537  dfmpq2  7538  enqbreq2  7540  enqdc  7544  addcmpblnq  7550  addpipqqslem  7552  mulpipq2  7554  mulpipq  7555  mulpipqqs  7556  addclnq  7558  distrnqg  7570  ltdcnq  7580  ltrnqg  7603  enq0breq  7619  addclnq0  7634  nqnq0a  7637  nqnq0m  7638  nq0m0r  7639  distrnq0  7642  mulcomnq0  7643  genipv  7692  genplt2i  7693  genpelvl  7695  genpelvu  7696  addnqprlemrl  7740  addnqprlemru  7741  addnqprlemfl  7742  addnqprlemfu  7743  addnqpr  7744  mulnqprlemrl  7756  mulnqprlemru  7757  mulnqprlemfl  7758  mulnqprlemfu  7759  mulnqpr  7760  distrlem4prl  7767  distrlem4pru  7768  ltnqpr  7776  recexprlemloc  7814  archrecnq  7846  mulclsr  7937  1idsr  7951  00sr  7952  prsradd  7969  axmulass  8056  axdistr  8057  axcnre  8064  peano5nnnn  8075  mulrid  8139  axltadd  8212  lenlt  8218  cnegexlem3  8319  cnegex  8320  resubcl  8406  subeqrev  8518  muladd  8526  mulsub  8543  mulsub2  8544  ltaddsub2  8580  leaddsub2  8582  leltadd  8590  ltaddpos2  8596  posdif  8598  addge02  8616  mullt0  8623  recexre  8721  recextlem1  8794  recexap  8796  divmuldivap  8855  conjmulap  8872  div2subap  8980  prodgt02  8996  prodge02  8998  lemul2  9000  lemul2a  9002  ltmulgt12  9008  lemulge12  9010  ltmuldiv2  9018  ltdivmul2  9021  ledivmul2  9023  lemuldiv2  9025  negiso  9098  cju  9104  peano5nni  9109  nnaddcl  9126  nnmulcl  9127  nnsub  9145  addltmul  9344  avgle1  9348  avgle2  9349  nnrecl  9363  nn0nnaddcl  9396  zsubcl  9483  zleloe  9489  znnsub  9494  nzadd  9495  zmulcl  9496  zltp1le  9497  zleltp1  9498  nnleltp1  9502  nnltp1le  9503  nnaddm1cl  9504  nn0ltp1le  9505  nn0leltp1  9506  nn0ltlem1  9507  znn0sub  9508  nn0sub  9509  elz2  9514  zapne  9517  zdcle  9519  zdclt  9520  zltlen  9521  nn0lem1lt  9526  nnlem1lt  9527  nnltlem1  9528  zdiv  9531  zextle  9534  zextlt  9535  btwnnz  9537  prime  9542  nneo  9546  peano2uz2  9550  peano5uzti  9551  uzind  9554  fzind  9558  fnn0ind  9559  uzneg  9737  uz11  9741  eluzp1m1  9742  eluzp1p1  9744  uzin  9751  indstr  9784  uz2mulcl  9799  qre  9816  qaddcl  9826  qsubcl  9829  qltlen  9831  qlttri2  9832  irradd  9837  elpqb  9841  cnref1o  9842  rpaddcl  9869  rpmulcl  9870  rpdivcl  9871  rexadd  10044  rexsub  10045  xaddcom  10053  xnn0xadd0  10059  xnegdi  10060  elicc2  10130  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  fzval2  10203  elfz1eq  10227  peano2fzr  10229  fznlem  10233  fzsplit2  10242  fzaddel  10251  fzsubel  10252  fzrev2  10277  fzrev3  10279  uzsplit  10284  fzrevral  10297  fzrevral3  10299  fzshftral  10300  elfz2nn0  10304  fznn0sub2  10320  fz0fzdiffz0  10322  elfzmlbp  10324  difelfzle  10326  difelfznle  10327  1fv  10331  elfzouz2  10354  fzo0n  10360  fzouzsplit  10373  fzoun  10375  elfzo0le  10381  fzonmapblen  10383  fzofzim  10384  fzoaddel2  10391  eluzgtdifelfzo  10398  elfzodifsumelfzo  10402  ubmelm1fzo  10427  fzofzp1b  10429  fzosplitprm1  10435  fzostep1  10438  subfzo0  10443  zsupcllemstep  10444  qdclt  10460  qbtwnxr  10472  flqbi2  10506  divfl0  10511  flqzadd  10513  flqmulnn0  10514  addmodidr  10590  modfzo0difsn  10612  frec2uzltd  10620  frec2uzrand  10622  frecfzen2  10644  seqshft2g  10699  seq3split  10705  seqsplitg  10706  seq3caopr2  10710  seqcaopr2g  10711  seqf1oglem2  10737  exp3vallem  10757  expcllem  10767  expcl2lemap  10768  1exp  10785  expge1  10793  expadd  10798  expmul  10801  expsubap  10804  leexp1a  10811  lt2sq  10830  le2sq  10831  sumsqeq0  10835  qsqeqor  10867  bernneq  10877  bernneq2  10878  sq11ap  10924  facdiv  10955  faclbnd  10958  faclbnd3  10960  faclbnd6  10961  facavg  10963  bcrpcl  10970  bccmpl  10971  fiubm  11045  seq3coll  11059  eqwrd  11107  ccatcl  11123  ccatclab  11124  ccatlen  11125  ccat0  11126  ccatval1  11127  ccatval2  11128  elfzelfzccat  11130  ccatvalfn  11131  ccatsymb  11132  ccatval21sw  11135  ccatrn  11139  lswccatn0lsw  11141  swrdfv2  11190  swrdsbslen  11193  swrdspsleq  11194  swrdccat2  11198  pfxclz  11206  ccatpfx  11228  pfxccat1  11229  swrdswrdlem  11231  pfxswrd  11233  pfxccatin12lem4  11253  pfxccatin12lem1  11255  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccat3  11261  swrdccat  11262  pfxccatpfx2  11264  pfxccat3a  11265  swrdccat3blem  11266  swrdccat3b  11267  s2dmg  11317  shftfvalg  11324  shftf  11336  crre  11363  crim  11364  mulreap  11370  readd  11375  resub  11376  remul2  11379  imadd  11383  imsub  11384  immul2  11386  ipcnval  11392  cjsub  11398  cjreim  11409  caucvgre  11487  rexanuz  11494  rexuz3  11496  resqrexlemover  11516  resqrexlemcvg  11525  resqrexlemglsq  11528  sqrtle  11542  sqrtlt  11543  sqrt11ap  11544  sqrt11  11545  absreimsq  11573  absreim  11574  absmul  11575  sqabs  11588  absdiflt  11598  absdifle  11599  abssuble0  11609  abs2difabs  11614  fzomaxdif  11619  caubnd2  11623  rpmaxcl  11729  zmaxcl  11730  nn0maxcl  11731  minmax  11736  mincl  11737  min1inf  11738  min2inf  11739  minabs  11742  minclpr  11743  rpmincl  11744  2zinfmin  11749  xrmaxrecl  11761  xrminmax  11771  xrmincl  11772  xrmin1inf  11773  xrmin2inf  11774  xrminrecl  11779  xrminrpcl  11780  iooinsup  11783  climconst2  11797  climuni  11799  2clim  11807  climshft  11810  climshft2  11812  cjcn2  11822  climaddc1  11835  climmulc2  11837  climsubc1  11838  climsubc2  11839  climlec2  11847  summodclem2a  11887  zsumdc  11890  isumclim3  11929  mptfzshft  11948  fsumrev  11949  fisum0diag2  11953  telfsumo2  11973  fsumparts  11976  cvgcmpub  11982  binomlem  11989  binom1p  11991  binom1dif  11993  bcxmas  11995  isumshft  11996  expcnvap0  12008  expcnv  12010  geosergap  12012  geolim  12017  cvgratnnlemrate  12036  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodmodc  12084  zproddc  12085  fprodf1o  12094  fprodeq0  12123  efcj  12179  eftlub  12196  effsumlt  12198  efieq  12241  sinsub  12246  cossub  12247  subsin  12249  sinmul  12250  cosmul  12251  addcos  12252  subcos  12253  dvdssub2  12341  dvdsadd  12342  dvdsaddr  12343  dvdssub  12344  dvdssubr  12345  fzocongeq  12364  odd2np1  12379  opoe  12401  omoe  12402  opeo  12403  omeo  12404  divalgb  12431  ndvdsadd  12437  bitsfi  12463  gcdmndc  12471  gcdabs  12504  dvdsgcd  12528  absmulgcd  12533  gcdmultiple  12536  gcdmultiplez  12537  rpmulgcd  12542  sqgcd  12545  dvdssqlem  12546  dvdssq  12547  nninfctlemfo  12556  nn0seqcvgd  12558  ialgrlemconst  12560  algrf  12562  algrp1  12563  algcvg  12565  algcvga  12568  lcmval  12580  lcmabs  12593  lcmgcd  12595  lcmdvds  12596  lcmgcdnn  12599  coprmgcdb  12605  coprmdvds  12609  coprmdvds2  12610  qredeq  12613  isprm3  12635  nprm  12640  divgcdodd  12660  prmdvdsexp  12665  sqrt2irr  12679  zgcdsq  12718  hashdvds  12738  phiprmpw  12739  crth  12741  phimullem  12742  modprm0  12772  coprimeprodsq  12775  coprimeprodsq2  12776  pythagtriplem2  12784  pythagtriplem19  12800  pcdvdsb  12838  pcneg  12843  pc2dvds  12848  pc11  12849  pcmpt  12861  pcfac  12868  infpnlem1  12877  prmunb  12880  1arithlem4  12884  1arith  12885  gzaddcl  12895  gzmulcl  12896  gzreim  12897  gzsubcl  12898  4sqlem1  12906  4sqlem4a  12909  4sqlem4  12910  4sqlem12  12920  setsvalg  13057  setsfun0  13063  restval  13273  xpsval  13380  mndinvmod  13473  resmhm  13515  resmhm2  13516  mhmco  13518  dfgrp3m  13627  mhmmnd  13648  mulgnngsum  13659  mulgnn0z  13681  mulgnndir  13683  ghmex  13787  0ghm  13790  resghm  13792  resghm2  13793  ghmco  13796  ghmeql  13799  kerf1ghm  13806  ablsubsub23  13857  dfrhm2  14112  isrhm  14116  rhmfn  14130  rhmval  14131  rhmco  14132  resrhm  14206  rhmeql  14208  rhmima  14209  lmodfopne  14284  lspf  14347  znidom  14615  znrrg  14618  innei  14831  cnovex  14864  txuni2  14924  txbasex  14925  txbas  14926  txtop  14928  txtopon  14930  txss12  14934  txbasval  14935  txcnp  14939  upxp  14940  txcnmpt  14941  uptx  14942  txcn  14943  txrest  14944  txdis  14945  cnmpt21  14959  hmeoco  14984  txhmeo  14987  isxmet2d  15016  blin2  15100  comet  15167  metcn  15182  txmetcn  15187  qtopbasss  15189  qtopbas  15190  remetdval  15215  bl2ioo  15218  blssioo  15221  divcnap  15233  cncfmet  15260  dvaddxxbr  15369  dvcjbr  15376  plyf  15405  ply1termlem  15410  plymullem1  15416  plyaddlem  15417  plymullem  15418  plycolemc  15426  plyreres  15432  dvply1  15433  efle  15444  reapef  15446  sinperlem  15476  sincosq2sgn  15495  sincosq3sgn  15496  sincos6thpi  15510  ioocosf1o  15522  relogoprlem  15536  logleb  15543  cxple3  15589  cxpcom  15606  dvdsppwf1o  15657  fsumdvdsmul  15659  1sgmprm  15662  mersenne  15665  lgslem3  15675  lgsdir2  15706  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  gausslemma2dlem1a  15731  gausslemma2dlem3  15736  gausslemma2dlem6  15740  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2  15756  lgsquad3  15757  2lgslem1a1  15759  2lgslem1a  15761  2lgslem1c  15763  2sqlem2  15788  mul2sq  15789  2sqlem7  15794  usgredg2v  16016  ushgredgedg  16018  ushgredgedgloop  16020  bj-inex  16228  bj-bdfindis  16268  triap  16356  cvgcmp2nlemabs  16359  trilpolemisumle  16365  inffz  16399