Theorem syl2anr 598

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 597	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 458	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  swopo  5544  ordintdif  6369  funco  6533  resdif  6796  fvcofneq  7040  fnprb  7156  fntpb  7157  fvf1pr  7255  isotr  7284  weisoeq  7303  brrpssg  7672  findsg  7841  coexg  7873  resf1extb  7878  xpexgALT  7927  fnsuppres  8135  oaass  8490  oeword  8520  oeworde  8523  mapsnd  8828  ixpssmapg  8870  enrefnn  8987  pw2f1olem  9013  domsdomtr  9044  xpen  9072  mapen  9073  mapdom1  9074  phplem2  9133  mapfienlem1  9312  elfir  9322  wdomen2  9486  carden2b  9883  harcard  9894  isinffi  9908  acnlem  9962  acndom  9965  alephdom  9995  fin23lem21  10253  fin23lem39  10264  isf32lem5  10271  fin1a2lem12  10325  axdc3lem2  10365  ttukeylem1  10423  pwcfsdom  10498  canthp1  10569  nqereu  10844  addpqf  10859  axmulf  11061  axmulass  11072  axdistr  11073  ltaddnegr  11354  negeu  11374  fimaxre3  12092  nnsub  12193  nn0sub  12455  ltsubnn0  12456  elz2  12510  uzaddcl  12821  qaddcl  12882  xltneg  13136  xleneg  13137  supxrbnd1  13240  infxrgelb  13255  iccneg  13392  uzsubsubfz  13466  fzsplit2  13469  fzadd2  13479  fzss1  13483  uzsplit  13516  fzdif1  13525  fz0fzdiffz0  13557  difelfzle  13561  difelfznle  13562  fvffz0  13566  preduz  13570  predfz  13573  fzonlt0  13602  fzouzsplit  13614  fzo0addelr  13639  eluzgtdifelfzo  13647  elfzodifsumelfzo  13651  ssfzo12  13679  elfznelfzob  13694  fllt  13730  flflp1  13731  uzsup  13787  negmod  13843  modifeq2int  13860  modfzo0difsn  13870  modsumfzodifsn  13871  om2uzlt2i  13878  nn0ennn  13906  suppssfz  13921  seqfveq2  13951  sermono  13961  seqf1o  13970  ser1const  13985  rpexpmord  14095  mulsubdivbinom2  14189  faclbnd  14217  bcval4  14234  bcpasc  14248  hashkf  14259  hashunx  14313  fz1isolem  14388  ishashinf  14390  seqcoll  14391  ccatval1  14504  ccatval21sw  14513  ccatrn  14517  ccatalpha  14521  swrdnd0  14585  swrd0  14586  swrdfv2  14589  swrdspsleq  14593  addlenpfx  14618  ccatpfx  14628  swrdswrd  14632  pfxccatin12lem2  14658  pfxccat3  14661  swrdccat  14662  revccat  14693  repswswrd  14711  cshwmodn  14722  cshwidxmod  14730  repswcshw  14739  2cshwid  14741  2cshwcom  14743  2cshwcshw  14752  cshwcshid  14754  cshwcsh2id  14755  s1co  14760  cshco  14763  trclub  14925  shftfval  14997  seqshft  15012  crim  15042  caubnd  15286  limsuplt  15406  isercolllem2  15593  fsumcvg  15639  fsumcvg2  15654  fsumshftm  15708  fsumo1  15739  isumshft  15766  harmonic  15786  cvgrat  15810  mertenslem1  15811  zprod  15864  fprodmodd  15924  bpolylem  15975  bpolysum  15980  bpolydiflem  15981  fsumkthpow  15983  rpnnen2lem12  16154  dvdsval3  16187  negdvdsb  16203  dvdsnegb  16204  dvdsmul1  16208  dvdsabseq  16244  dvdsssfz1  16249  odd2np1  16272  divalglem8  16331  ndvdsadd  16341  dfgcd2  16477  dvdssqim  16485  nn0seqcvgd  16501  seq1st  16502  algcvgblem  16508  lcmf  16564  lcmfunsnlem2  16571  cncongr2  16599  prmdvdsfz  16636  isprm7  16639  prmndvdsfaclt  16656  powm2modprm  16735  modprm0  16737  modprmn0modprm0  16739  pythagtriplem1  16748  pythagtriplem4  16751  pythagtriplem8  16755  pythagtriplem9  16756  pythagtriplem12  16758  pythagtriplem14  16760  pythagtriplem16  16762  pcexp  16791  pc2dvds  16811  pcz  16813  fldivp1  16829  pcfac  16831  oddprmdvds  16835  pockthg  16838  infpnlem1  16842  prmreclem1  16848  prmreclem2  16849  1arith  16859  4sqlem11  16887  vdwlem2  16914  vdwlem8  16920  vdwnnlem2  16928  prmgaplem7  16989  prmgaplem8  16990  cshwshashlem2  17028  cshwshashlem3  17029  pwsval  17410  isacs1i  17584  funcsetcestrclem9  18090  ismgmid  18594  mgmhmpropd  18627  mhmpropd  18721  smndex1gid  18832  smndex1id  18840  grpsubid1  18959  mulgnnp1  19016  mulgsubcl  19022  mulgnn0z  19035  mulgnndir  19037  mulgneg2  19042  lagsubg  19128  ghmco  19169  symg2bas  19326  symgextfv  19351  pgpfi2  19539  efgsfo  19672  frgpupf  19706  frgpup1  19708  gsummptshft  19869  telgsumfzslem  19921  telgsums  19926  ablfac1eu  20008  pgpfac1lem2  20010  ablfaclem3  20022  dvdsrid  20307  dvdsrneg  20310  dvr1  20347  abv1  20762  lmodfopne  20855  lbsexg  21123  xrsds  21368  znf1o  21510  lindfmm  21786  gsummoncoe1  22256  matecl  22373  mavmul0g  22501  gsummatr01  22607  mp2pm2mplem4  22757  chfacfisf  22802  chfacfisfcpmat  22803  chfacfpmmulgsum2  22813  cpmadugsumlemF  22824  isclo  23035  resttopon  23109  restcld  23120  restcls  23129  iscn  23183  iscnp  23185  cnco  23214  cndis  23239  cnindis  23240  cmpsub  23348  hauscmplem  23354  cmpfii  23357  ptcnplem  23569  txtube  23588  txcmplem1  23589  xkoptsub  23602  qtoptop  23648  kqfval  23671  hmeoco  23720  fileln0  23798  trfil1  23834  trfil2  23835  trufil  23858  elfm3  23898  hausflf2  23946  isucn  24225  bl2in  24348  metss2lem  24459  metss2  24460  stdbdxmet  24463  metrest  24472  nmval2  24540  nmoix  24677  ioo2bl  24741  xrsxmet  24758  expcn  24823  expcnOLD  24825  elcncf  24842  icccvx  24908  cphsscph  25211  iscmet3  25253  causs  25258  metcld2  25267  metsscmetcld  25275  cncmet  25282  bcth3  25291  ovolgelb  25441  ovolfi  25455  shft2rab  25469  uniioombllem3  25546  dyadmax  25559  dyadmbl  25561  subopnmbl  25565  volcn  25567  mbfid  25596  mbfeqalem2  25603  mbfres  25605  cnmbf  25620  i1fmulc  25664  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  itg2seq  25703  itg2gt0  25721  itgss3  25776  dvexp  25917  plypow  26170  plyeq0lem  26175  coeidlem  26202  dgrlt  26232  dgrcolem2  26240  elqaalem2  26288  aacjcl  26295  aaliou3lem1  26310  aaliou3lem2  26311  pserdvlem2  26398  abelthlem8  26409  cosord  26500  sinord  26503  resinf1o  26505  relogexp  26565  logdivlt  26590  advlogexp  26624  logcxp  26638  cxpcl  26643  rpcxpcl  26645  cxpne0  26646  logbchbase  26741  logbgt0b  26763  birthdaylem2  26922  cxplim  26942  divsqrtsumo1  26954  zetacvg  26985  wilthlem1  27038  ftalem7  27049  basellem1  27051  issqf  27106  sqf11  27109  sgmf  27115  sgmnncl  27117  sqff1o  27152  dvdsflsumcom  27158  mpodvdsmulf1o  27164  dvdsmulf1o  27166  sgmppw  27168  chtublem  27182  chtub  27183  logexprlim  27196  bposlem3  27257  bposlem5  27259  bposlem6  27260  lgsdirnn0  27315  gausslemma2dlem1a  27336  gausslemma2dlem5a  27341  lgsquad2  27357  lgsquad3  27358  2sqreulem1  27417  2sqreunnlem1  27420  dchrisumlem1  27460  dchrisumlem2  27461  dchrisumlem3  27462  mulogsumlem  27502  noextenddif  27640  addsrid  27946  sltneg  28027  sleneg  28028  om2noseqlt2  28281  elzn0s  28377  eln0zs  28379  peano5uzs  28383  brbtwn  28955  uspgrupgrushgr  29235  usgrumgruspgr  29238  cusgrfilem2  29513  finsumvtxdg2ssteplem2  29603  cyclnumvtx  29856  crctcshwlkn0lem4  29869  crctcshwlkn0lem6  29871  crctcshwlkn0lem7  29872  crctcshwlkn0  29877  elwspths2spth  30026  rusgrnumwwlk  30034  clwlkclwwlklem2fv2  30054  erclwwlknref  30127  1to2vfriswmgr  30337  4cycl2v2nb  30347  frgr2wwlkeqm  30389  nvo00  30819  nmorepnf  30826  ubthlem1  30928  normpyc  31204  occon3  31355  pjpreeq  31456  idcnop  32039  riesz3i  32120  cnlnssadj  32138  rnbra  32165  strlem3a  32310  cvcon3  32342  ssdmd1  32371  ssdmd2  32372  relfi  32659  fcobijfs2  32782  fzsplit3  32854  prmsimpcyc  33291  esumcst  34201  dmvlsiga  34267  ballotlemimin  34644  bnj545  35032  bnj929  35073  bnj953  35076  fineqvnttrclselem1  35258  pthhashvtx  35303  derangsn  35345  iscvm  35434  cvmsval  35441  cvmliftlem7  35466  cvmlift2lem12  35489  mclsssvlem  35737  supfz  35904  faclimlem3  35920  opnrebl2  36496  nn0prpwlem  36497  tailval  36548  nndivlub  36633  ctbssinf  37582  finixpnum  37777  ltflcei  37780  lindsdom  37786  lindsenlbs  37787  matunitlindflem2  37789  poimirlem4  37796  poimirlem14  37806  poimirlem15  37807  poimirlem19  37811  poimirlem20  37812  poimirlem22  37814  poimirlem24  37816  poimirlem28  37820  poimirlem30  37822  poimirlem31  37823  mblfinlem2  37830  mblfinlem3  37831  mblfinlem4  37832  ftc1anclem1  37865  ftc1anclem4  37868  ftc1anclem5  37869  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873  caushft  37933  ismtyval  37972  heiborlem7  37989  heiborlem10  37992  heibor  37993  lcmineqlem8  42327  deg1gprod  42431  f1o2d2  42526  oexpreposd  42613  elrfirn  42973  ismrc  42979  nacsfix  42990  mzpcompact2lem  43029  eldiophb  43035  ellz1  43045  rexrabdioph  43072  congrep  43251  jm2.26a  43278  rngunsnply  43447  mendring  43466  iocmbl  43491  oeord2lim  43587  cantnfresb  43602  omabs2  43610  ofoafg  43632  dfno2  43705  rp-isfinite5  43794  enrelmap  44274  expgrowthi  44610  cnfex  45309  xlimclim2lem  46119  climxlim2  46126  icccncfext  46167  itgsinexp  46235  iblspltprt  46253  itgspltprt  46259  fourierdlem50  46436  fourierswlem  46510  etransclem35  46549  zm1nn  47584  subsubelfzo0  47608  ceilbi  47615  addmodne  47626  m1modmmod  47640  modlt0b  47645  iccpartres  47700  iccelpart  47715  iccpartiun  47716  iccpartnel  47720  goldbachthlem1  47827  goldbachth  47829  odz2prm2pw  47845  2pwp1prm  47871  evenltle  47999  fpprwpprb  48022  sbgoldbaltlem2  48062  bgoldbachlt  48095  isubgredg  48148  gricushgr  48199  uhgrimisgrgriclem  48212  gpgvtx0  48335  gpg5nbgrvtx13starlem2  48354  upgrwlkupwlk  48422  2zrngamgm  48527  lincresunit3  48763  lincreslvec3  48764  isldepslvec2  48767  blengt1fldiv2p1  48875  dignn0flhalf  48900  nn0sumshdiglemA  48901  rrx2pnedifcoorneor  48998  precofval2  49650  aacllem  50082