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  944  mp3an3an  1358  eqeqan12d  2225  sylan9eq  2262  csbcomg  3127  sylan9ss  3217  ssconb  3317  ineqan12d  3387  dfopg  3834  breqan12d  4078  opexg  4293  copsex2g  4311  ordin  4453  onin  4454  unexg  4511  eusv1  4520  opelvvg  4745  opthprc  4747  opbrop  4775  relop  4849  dmpropg  5177  unixpm  5240  funssres  5336  funinsn  5346  funtp  5350  fnco  5407  resasplitss  5481  fodmrnu  5532  relrnfvex  5621  funopdmsn  5792  fconst2g  5827  oveqan12d  5993  ovi3  6113  ovg  6115  f1opw2  6182  off  6201  offres  6250  iunon  6400  nnsucsssuc  6608  nnaword1  6629  ertr  6665  erex  6674  brecop  6742  ecovdi  6763  ecovidi  6764  mapvalg  6775  pmvalg  6776  pmss12g  6792  mapsn  6807  en2sn  6936  xpf1o  6973  xpen  6974  phplem4  6984  ssfilem  7005  diffitest  7017  en1eqsn  7083  sbthlem7  7098  ordiso  7171  updjud  7217  fodju0  7282  finnum  7323  pr2nelem  7332  djucomen  7366  exmidontriimlem1  7371  2onetap  7409  ltsopi  7475  pitric  7476  pitri3or  7477  ltdcpi  7478  mulclpi  7483  addcompig  7484  mulcompig  7486  distrpig  7488  ltexpi  7492  ltapig  7493  ltmpig  7494  dfplpq2  7509  dfmpq2  7510  enqbreq2  7512  enqdc  7516  addcmpblnq  7522  addpipqqslem  7524  mulpipq2  7526  mulpipq  7527  mulpipqqs  7528  addclnq  7530  distrnqg  7542  ltdcnq  7552  ltrnqg  7575  enq0breq  7591  addclnq0  7606  nqnq0a  7609  nqnq0m  7610  nq0m0r  7611  distrnq0  7614  mulcomnq0  7615  genipv  7664  genplt2i  7665  genpelvl  7667  genpelvu  7668  addnqprlemrl  7712  addnqprlemru  7713  addnqprlemfl  7714  addnqprlemfu  7715  addnqpr  7716  mulnqprlemrl  7728  mulnqprlemru  7729  mulnqprlemfl  7730  mulnqprlemfu  7731  mulnqpr  7732  distrlem4prl  7739  distrlem4pru  7740  ltnqpr  7748  recexprlemloc  7786  archrecnq  7818  mulclsr  7909  1idsr  7923  00sr  7924  prsradd  7941  axmulass  8028  axdistr  8029  axcnre  8036  peano5nnnn  8047  mulrid  8111  axltadd  8184  lenlt  8190  cnegexlem3  8291  cnegex  8292  resubcl  8378  subeqrev  8490  muladd  8498  mulsub  8515  mulsub2  8516  ltaddsub2  8552  leaddsub2  8554  leltadd  8562  ltaddpos2  8568  posdif  8570  addge02  8588  mullt0  8595  recexre  8693  recextlem1  8766  recexap  8768  divmuldivap  8827  conjmulap  8844  div2subap  8952  prodgt02  8968  prodge02  8970  lemul2  8972  lemul2a  8974  ltmulgt12  8980  lemulge12  8982  ltmuldiv2  8990  ltdivmul2  8993  ledivmul2  8995  lemuldiv2  8997  negiso  9070  cju  9076  peano5nni  9081  nnaddcl  9098  nnmulcl  9099  nnsub  9117  addltmul  9316  avgle1  9320  avgle2  9321  nnrecl  9335  nn0nnaddcl  9368  zsubcl  9455  zleloe  9461  znnsub  9466  nzadd  9467  zmulcl  9468  zltp1le  9469  zleltp1  9470  nnleltp1  9474  nnltp1le  9475  nnaddm1cl  9476  nn0ltp1le  9477  nn0leltp1  9478  nn0ltlem1  9479  znn0sub  9480  nn0sub  9481  elz2  9486  zapne  9489  zdcle  9491  zdclt  9492  zltlen  9493  nn0lem1lt  9498  nnlem1lt  9499  nnltlem1  9500  zdiv  9503  zextle  9506  zextlt  9507  btwnnz  9509  prime  9514  nneo  9518  peano2uz2  9522  peano5uzti  9523  uzind  9526  fzind  9530  fnn0ind  9531  uzneg  9709  uz11  9713  eluzp1m1  9714  eluzp1p1  9716  uzin  9723  indstr  9756  uz2mulcl  9771  qre  9788  qaddcl  9798  qsubcl  9801  qltlen  9803  qlttri2  9804  irradd  9809  elpqb  9813  cnref1o  9814  rpaddcl  9841  rpmulcl  9842  rpdivcl  9843  rexadd  10016  rexsub  10017  xaddcom  10025  xnn0xadd0  10031  xnegdi  10032  elicc2  10102  iccshftr  10158  iccshftl  10160  iccdil  10162  icccntr  10164  fzval2  10175  elfz1eq  10199  peano2fzr  10201  fznlem  10205  fzsplit2  10214  fzaddel  10223  fzsubel  10224  fzrev2  10249  fzrev3  10251  uzsplit  10256  fzrevral  10269  fzrevral3  10271  fzshftral  10272  elfz2nn0  10276  fznn0sub2  10292  fz0fzdiffz0  10294  elfzmlbp  10296  difelfzle  10298  difelfznle  10299  1fv  10303  elfzouz2  10326  fzo0n  10332  fzouzsplit  10345  fzoun  10347  elfzo0le  10353  fzonmapblen  10355  fzofzim  10356  fzoaddel2  10363  eluzgtdifelfzo  10370  elfzodifsumelfzo  10374  ubmelm1fzo  10399  fzofzp1b  10401  fzosplitprm1  10407  fzostep1  10410  subfzo0  10415  zsupcllemstep  10416  qdclt  10432  qbtwnxr  10444  flqbi2  10478  divfl0  10483  flqzadd  10485  flqmulnn0  10486  addmodidr  10562  modfzo0difsn  10584  frec2uzltd  10592  frec2uzrand  10594  frecfzen2  10616  seqshft2g  10671  seq3split  10677  seqsplitg  10678  seq3caopr2  10682  seqcaopr2g  10683  seqf1oglem2  10709  exp3vallem  10729  expcllem  10739  expcl2lemap  10740  1exp  10757  expge1  10765  expadd  10770  expmul  10773  expsubap  10776  leexp1a  10783  lt2sq  10802  le2sq  10803  sumsqeq0  10807  qsqeqor  10839  bernneq  10849  bernneq2  10850  sq11ap  10896  facdiv  10927  faclbnd  10930  faclbnd3  10932  faclbnd6  10933  facavg  10935  bcrpcl  10942  bccmpl  10943  fiubm  11017  seq3coll  11031  eqwrd  11078  ccatcl  11094  ccatclab  11095  ccatlen  11096  ccat0  11097  ccatval1  11098  ccatval2  11099  elfzelfzccat  11101  ccatvalfn  11102  ccatsymb  11103  ccatval21sw  11106  ccatrn  11110  lswccatn0lsw  11112  swrdfv2  11161  swrdsbslen  11164  swrdspsleq  11165  swrdccat2  11169  pfxclz  11177  ccatpfx  11199  pfxccat1  11200  swrdswrdlem  11202  pfxswrd  11204  pfxccatin12lem4  11224  pfxccatin12lem1  11226  pfxccatin12lem2  11229  pfxccatin12lem3  11230  pfxccat3  11232  swrdccat  11233  pfxccatpfx2  11235  pfxccat3a  11236  swrdccat3blem  11237  swrdccat3b  11238  s2dmg  11288  shftfvalg  11295  shftf  11307  crre  11334  crim  11335  mulreap  11341  readd  11346  resub  11347  remul2  11350  imadd  11354  imsub  11355  immul2  11357  ipcnval  11363  cjsub  11369  cjreim  11380  caucvgre  11458  rexanuz  11465  rexuz3  11467  resqrexlemover  11487  resqrexlemcvg  11496  resqrexlemglsq  11499  sqrtle  11513  sqrtlt  11514  sqrt11ap  11515  sqrt11  11516  absreimsq  11544  absreim  11545  absmul  11546  sqabs  11559  absdiflt  11569  absdifle  11570  abssuble0  11580  abs2difabs  11585  fzomaxdif  11590  caubnd2  11594  rpmaxcl  11700  zmaxcl  11701  nn0maxcl  11702  minmax  11707  mincl  11708  min1inf  11709  min2inf  11710  minabs  11713  minclpr  11714  rpmincl  11715  2zinfmin  11720  xrmaxrecl  11732  xrminmax  11742  xrmincl  11743  xrmin1inf  11744  xrmin2inf  11745  xrminrecl  11750  xrminrpcl  11751  iooinsup  11754  climconst2  11768  climuni  11770  2clim  11778  climshft  11781  climshft2  11783  cjcn2  11793  climaddc1  11806  climmulc2  11808  climsubc1  11809  climsubc2  11810  climlec2  11818  summodclem2a  11858  zsumdc  11861  isumclim3  11900  mptfzshft  11919  fsumrev  11920  fisum0diag2  11924  telfsumo2  11944  fsumparts  11947  cvgcmpub  11953  binomlem  11960  binom1p  11962  binom1dif  11964  bcxmas  11966  isumshft  11967  expcnvap0  11979  expcnv  11981  geosergap  11983  geolim  11988  cvgratnnlemrate  12007  mertenslemi1  12012  mertenslem2  12013  mertensabs  12014  prodmodc  12055  zproddc  12056  fprodf1o  12065  fprodeq0  12094  efcj  12150  eftlub  12167  effsumlt  12169  efieq  12212  sinsub  12217  cossub  12218  subsin  12220  sinmul  12221  cosmul  12222  addcos  12223  subcos  12224  dvdssub2  12312  dvdsadd  12313  dvdsaddr  12314  dvdssub  12315  dvdssubr  12316  fzocongeq  12335  odd2np1  12350  opoe  12372  omoe  12373  opeo  12374  omeo  12375  divalgb  12402  ndvdsadd  12408  bitsfi  12434  gcdmndc  12442  gcdabs  12475  dvdsgcd  12499  absmulgcd  12504  gcdmultiple  12507  gcdmultiplez  12508  rpmulgcd  12513  sqgcd  12516  dvdssqlem  12517  dvdssq  12518  nninfctlemfo  12527  nn0seqcvgd  12529  ialgrlemconst  12531  algrf  12533  algrp1  12534  algcvg  12536  algcvga  12539  lcmval  12551  lcmabs  12564  lcmgcd  12566  lcmdvds  12567  lcmgcdnn  12570  coprmgcdb  12576  coprmdvds  12580  coprmdvds2  12581  qredeq  12584  isprm3  12606  nprm  12611  divgcdodd  12631  prmdvdsexp  12636  sqrt2irr  12650  zgcdsq  12689  hashdvds  12709  phiprmpw  12710  crth  12712  phimullem  12713  modprm0  12743  coprimeprodsq  12746  coprimeprodsq2  12747  pythagtriplem2  12755  pythagtriplem19  12771  pcdvdsb  12809  pcneg  12814  pc2dvds  12819  pc11  12820  pcmpt  12832  pcfac  12839  infpnlem1  12848  prmunb  12851  1arithlem4  12855  1arith  12856  gzaddcl  12866  gzmulcl  12867  gzreim  12868  gzsubcl  12869  4sqlem1  12877  4sqlem4a  12880  4sqlem4  12881  4sqlem12  12891  setsvalg  13028  setsfun0  13034  restval  13244  xpsval  13351  mndinvmod  13444  resmhm  13486  resmhm2  13487  mhmco  13489  dfgrp3m  13598  mhmmnd  13619  mulgnngsum  13630  mulgnn0z  13652  mulgnndir  13654  ghmex  13758  0ghm  13761  resghm  13763  resghm2  13764  ghmco  13767  ghmeql  13770  kerf1ghm  13777  ablsubsub23  13828  dfrhm2  14083  isrhm  14087  rhmfn  14101  rhmval  14102  rhmco  14103  resrhm  14177  rhmeql  14179  rhmima  14180  lmodfopne  14255  lspf  14318  znidom  14586  znrrg  14589  innei  14802  cnovex  14835  txuni2  14895  txbasex  14896  txbas  14897  txtop  14899  txtopon  14901  txss12  14905  txbasval  14906  txcnp  14910  upxp  14911  txcnmpt  14912  uptx  14913  txcn  14914  txrest  14915  txdis  14916  cnmpt21  14930  hmeoco  14955  txhmeo  14958  isxmet2d  14987  blin2  15071  comet  15138  metcn  15153  txmetcn  15158  qtopbasss  15160  qtopbas  15161  remetdval  15186  bl2ioo  15189  blssioo  15192  divcnap  15204  cncfmet  15231  dvaddxxbr  15340  dvcjbr  15347  plyf  15376  ply1termlem  15381  plymullem1  15387  plyaddlem  15388  plymullem  15389  plycolemc  15397  plyreres  15403  dvply1  15404  efle  15415  reapef  15417  sinperlem  15447  sincosq2sgn  15466  sincosq3sgn  15467  sincos6thpi  15481  ioocosf1o  15493  relogoprlem  15507  logleb  15514  cxple3  15560  cxpcom  15577  dvdsppwf1o  15628  fsumdvdsmul  15630  1sgmprm  15633  mersenne  15636  lgslem3  15646  lgsdir2  15677  lgsdir  15679  lgsdilem2  15680  lgsdi  15681  gausslemma2dlem1a  15702  gausslemma2dlem3  15707  gausslemma2dlem6  15711  lgseisenlem3  15716  lgseisenlem4  15717  lgsquadlem1  15721  lgsquadlem2  15722  lgsquad2  15727  lgsquad3  15728  2lgslem1a1  15730  2lgslem1a  15732  2lgslem1c  15734  2sqlem2  15759  mul2sq  15760  2sqlem7  15765  usgredg2v  15987  ushgredgedg  15989  ushgredgedgloop  15991  bj-inex  16180  bj-bdfindis  16220  triap  16308  cvgcmp2nlemabs  16311  trilpolemisumle  16317  inffz  16351