Theorem syl2anr 600

Description: A double syllogism inference. For an implication-only version, see syl2imc 41. (Contributed by NM, 17-Sep-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem syl2anr

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an.2	. . 3 ⊢ (𝜏 → 𝜒)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	1, 2, 3	syl2an 599	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 462	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  swopo  5479  ordintdif  6262  funco  6420  resdif  6681  fvcofneq  6912  fnprb  7024  fntpb  7025  isotr  7145  weisoeq  7164  brrpssg  7513  findsg  7677  coexg  7707  xpexgALT  7754  fnsuppres  7933  wfrlem10  8064  oaass  8289  oeword  8318  oeworde  8321  mapsnd  8567  ixpssmapg  8609  enrefnn  8724  pw2f1olem  8749  domsdomtr  8781  xpen  8809  mapen  8810  mapdom1  8811  mapfienlem1  9021  elfir  9031  wdomen2  9193  carden2b  9583  harcard  9594  isinffi  9608  acnlem  9662  acndom  9665  alephdom  9695  fin23lem21  9953  fin23lem39  9964  isf32lem5  9971  fin1a2lem12  10025  axdc3lem2  10065  ttukeylem1  10123  pwcfsdom  10197  canthp1  10268  nqereu  10543  addpqf  10558  axmulf  10760  axmulass  10771  axdistr  10772  ltaddnegr  11048  negeu  11068  fimaxre3  11778  nnsub  11874  nn0sub  12140  ltsubnn0  12141  elz2  12194  uzaddcl  12500  qaddcl  12561  xltneg  12807  xleneg  12808  supxrbnd1  12911  infxrgelb  12925  iccneg  13060  uzsubsubfz  13134  fzsplit2  13137  fzadd2  13147  fzss1  13151  uzsplit  13184  fz0fzdiffz0  13221  difelfzle  13225  difelfznle  13226  fvffz0  13230  preduz  13234  predfz  13237  fzonlt0  13265  fzouzsplit  13277  fzo0addelr  13297  eluzgtdifelfzo  13304  elfzodifsumelfzo  13308  ssfzo12  13335  elfznelfzob  13348  fllt  13381  flflp1  13382  uzsup  13436  negmod  13489  modifeq2int  13506  modfzo0difsn  13516  modsumfzodifsn  13517  om2uzlt2i  13524  nn0ennn  13552  suppssfz  13567  seqfveq2  13598  sermono  13608  seqf1o  13617  ser1const  13632  rpexpmord  13738  mulsubdivbinom2  13828  faclbnd  13856  bcval4  13873  bcpasc  13887  hashkf  13898  hashunx  13953  hashfacenOLD  14019  fz1isolem  14027  ishashinf  14029  seqcoll  14030  ccatval1  14133  ccatval21sw  14142  ccatrn  14146  ccatalpha  14150  swrdnd0  14222  swrd0  14223  swrdfv2  14226  swrdspsleq  14230  addlenpfx  14256  ccatpfx  14266  swrdswrd  14270  pfxccatin12lem2  14296  pfxccat3  14299  swrdccat  14300  revccat  14331  repswswrd  14349  cshwmodn  14360  cshwidxmod  14368  repswcshw  14377  2cshwid  14379  2cshwcom  14381  2cshwcshw  14390  cshwcshid  14392  cshwcsh2id  14393  s1co  14398  cshco  14401  trclub  14561  shftfval  14633  seqshft  14648  crim  14678  caubnd  14922  limsuplt  15040  isercolllem2  15229  fsumcvg  15276  fsumcvg2  15291  fsumshftm  15345  fsumo1  15376  isumshft  15403  harmonic  15423  cvgrat  15447  mertenslem1  15448  zprod  15499  fprodmodd  15559  bpolylem  15610  bpolysum  15615  bpolydiflem  15616  fsumkthpow  15618  rpnnen2lem12  15786  dvdsval3  15819  negdvdsb  15834  dvdsnegb  15835  dvdsmul1  15839  dvdsabseq  15874  dvdsssfz1  15879  odd2np1  15902  divalglem8  15961  ndvdsadd  15971  dfgcd2  16106  dvdssqim  16116  nn0seqcvgd  16127  seq1st  16128  algcvgblem  16134  lcmf  16190  lcmfunsnlem2  16197  cncongr2  16225  prmdvdsfz  16262  isprm7  16265  prmndvdsfaclt  16282  powm2modprm  16356  modprm0  16358  modprmn0modprm0  16360  pythagtriplem1  16369  pythagtriplem4  16372  pythagtriplem8  16376  pythagtriplem9  16377  pythagtriplem12  16379  pythagtriplem14  16381  pythagtriplem16  16383  pcexp  16412  pc2dvds  16432  pcz  16434  fldivp1  16450  pcfac  16452  oddprmdvds  16456  pockthg  16459  infpnlem1  16463  prmreclem1  16469  prmreclem2  16470  1arith  16480  4sqlem11  16508  vdwlem2  16535  vdwlem8  16541  vdwnnlem2  16549  prmgaplem7  16610  prmgaplem8  16611  cshwshashlem2  16650  cshwshashlem3  16651  pwsval  16991  isacs1i  17160  funcsetcestrclem9  17670  ismgmid  18137  mhmpropd  18224  smndex1gid  18330  smndex1id  18338  grpsubid1  18448  mulgnnp1  18500  mulgsubcl  18506  mulgnn0z  18518  mulgnndir  18520  mulgneg2  18525  lagsubg  18606  ghmco  18642  symg2bas  18785  symgextfv  18810  pgpfi2  18995  efgsfo  19129  frgpupf  19163  frgpup1  19165  gsummptshft  19321  telgsumfzslem  19373  telgsums  19378  ablfac1eu  19460  pgpfac1lem2  19462  ablfaclem3  19474  dvdsrid  19669  dvdsrneg  19672  dvr1  19707  abv1  19869  lmodfopne  19937  lbsexg  20201  xrsds  20406  znf1o  20516  lindfmm  20789  gsummoncoe1  21225  matecl  21322  mavmul0g  21450  gsummatr01  21556  mp2pm2mplem4  21706  chfacfisf  21751  chfacfisfcpmat  21752  chfacfpmmulgsum2  21762  cpmadugsumlemF  21773  isclo  21984  resttopon  22058  restcld  22069  restcls  22078  iscn  22132  iscnp  22134  cnco  22163  cndis  22188  cnindis  22189  cmpsub  22297  hauscmplem  22303  cmpfii  22306  ptcnplem  22518  txtube  22537  txcmplem1  22538  xkoptsub  22551  qtoptop  22597  kqfval  22620  hmeoco  22669  fileln0  22747  trfil1  22783  trfil2  22784  trufil  22807  elfm3  22847  hausflf2  22895  isucn  23175  bl2in  23298  metss2lem  23409  metss2  23410  stdbdxmet  23413  metrest  23422  nmval2  23490  nmoix  23627  ioo2bl  23690  xrsxmet  23706  expcn  23769  elcncf  23786  icccvx  23847  cphsscph  24148  iscmet3  24190  causs  24195  metcld2  24204  metsscmetcld  24212  cncmet  24219  bcth3  24228  ovolgelb  24377  ovolfi  24391  shft2rab  24405  uniioombllem3  24482  dyadmax  24495  dyadmbl  24497  subopnmbl  24501  volcn  24503  mbfid  24532  mbfeqalem2  24539  mbfres  24541  cnmbf  24556  i1fmulc  24601  mbfi1fseqlem3  24615  mbfi1fseqlem4  24616  itg2seq  24640  itg2gt0  24658  itgss3  24712  dvexp  24850  plypow  25099  plyeq0lem  25104  coeidlem  25131  dgrlt  25160  dgrcolem2  25168  elqaalem2  25213  aacjcl  25220  aaliou3lem1  25235  aaliou3lem2  25236  pserdvlem2  25320  abelthlem8  25331  cosord  25420  sinord  25423  resinf1o  25425  relogexp  25484  logdivlt  25509  advlogexp  25543  logcxp  25557  cxpcl  25562  rpcxpcl  25564  cxpne0  25565  logbchbase  25654  logbgt0b  25676  birthdaylem2  25835  cxplim  25854  divsqrtsumo1  25866  zetacvg  25897  wilthlem1  25950  ftalem7  25961  basellem1  25963  issqf  26018  sqf11  26021  sgmf  26027  sgmnncl  26029  sqff1o  26064  dvdsflsumcom  26070  dvdsmulf1o  26076  sgmppw  26078  chtublem  26092  chtub  26093  logexprlim  26106  bposlem3  26167  bposlem5  26169  bposlem6  26170  lgsdirnn0  26225  gausslemma2dlem1a  26246  gausslemma2dlem5a  26251  lgsquad2  26267  lgsquad3  26268  2sqreulem1  26327  2sqreunnlem1  26330  dchrisumlem1  26370  dchrisumlem2  26371  dchrisumlem3  26372  mulogsumlem  26412  brbtwn  26990  uspgrupgrushgr  27268  usgrumgruspgr  27271  cusgrfilem2  27544  finsumvtxdg2ssteplem2  27634  crctcshwlkn0lem4  27897  crctcshwlkn0lem6  27899  crctcshwlkn0lem7  27900  crctcshwlkn0  27905  elwspths2spth  28051  rusgrnumwwlk  28059  clwlkclwwlklem2fv2  28079  erclwwlknref  28152  1to2vfriswmgr  28362  4cycl2v2nb  28372  frgr2wwlkeqm  28414  nvo00  28842  nmorepnf  28849  ubthlem1  28951  normpyc  29227  occon3  29378  pjpreeq  29479  idcnop  30062  riesz3i  30143  cnlnssadj  30161  rnbra  30188  strlem3a  30333  cvcon3  30365  ssdmd1  30394  ssdmd2  30395  relfi  30660  fzsplit3  30835  prmsimpcyc  31200  esumcst  31743  dmvlsiga  31809  ballotlemimin  32184  bnj545  32588  bnj929  32629  bnj953  32632  pthhashvtx  32802  derangsn  32845  iscvm  32934  cvmsval  32941  cvmliftlem7  32966  cvmlift2lem12  32989  mclsssvlem  33237  supfz  33412  faclimlem3  33429  noextenddif  33608  addsid1  33864  opnrebl2  34247  nn0prpwlem  34248  tailval  34299  nndivlub  34384  ctbssinf  35314  finixpnum  35499  ltflcei  35502  lindsdom  35508  lindsenlbs  35509  matunitlindflem2  35511  poimirlem4  35518  poimirlem14  35528  poimirlem15  35529  poimirlem19  35533  poimirlem20  35534  poimirlem22  35536  poimirlem24  35538  poimirlem28  35542  poimirlem30  35544  poimirlem31  35545  mblfinlem2  35552  mblfinlem3  35553  mblfinlem4  35554  ftc1anclem1  35587  ftc1anclem4  35590  ftc1anclem5  35591  ftc1anclem7  35593  ftc1anclem8  35594  ftc1anc  35595  caushft  35656  ismtyval  35695  heiborlem7  35712  heiborlem10  35715  heibor  35716  lcmineqlem8  39778  oexpreposd  40028  elrfirn  40220  ismrc  40226  nacsfix  40237  mzpcompact2lem  40276  eldiophb  40282  ellz1  40292  rexrabdioph  40319  congrep  40498  jm2.26a  40525  rngunsnply  40701  mendring  40720  iocmbl  40747  rp-isfinite5  40809  enrelmap  41282  expgrowthi  41624  cnfex  42244  xlimclim2lem  43055  climxlim2  43062  icccncfext  43103  itgsinexp  43171  iblspltprt  43189  itgspltprt  43195  fourierdlem50  43372  fourierswlem  43446  etransclem35  43485  zm1nn  44467  subsubelfzo0  44491  iccpartres  44543  iccelpart  44558  iccpartiun  44559  iccpartnel  44563  goldbachthlem1  44670  goldbachth  44672  odz2prm2pw  44688  2pwp1prm  44714  evenltle  44842  fpprwpprb  44865  sbgoldbaltlem2  44905  bgoldbachlt  44938  isomushgr  44951  isomuspgrlem1  44952  isomgrtr  44964  upgrwlkupwlk  44975  mgmhmpropd  45012  2zrngamgm  45170  lincresunit3  45495  lincreslvec3  45496  isldepslvec2  45499  m1modmmod  45540  blengt1fldiv2p1  45612  dignn0flhalf  45637  nn0sumshdiglemA  45638  rrx2pnedifcoorneor  45735  aacllem  46176