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  5551  ordintdif  6376  funco  6540  resdif  6803  fvcofneq  7047  fnprb  7164  fntpb  7165  fvf1pr  7263  isotr  7292  weisoeq  7311  brrpssg  7680  findsg  7849  coexg  7881  resf1extb  7886  xpexgALT  7935  fnsuppres  8143  oaass  8498  oeword  8528  oeworde  8531  mapsnd  8836  ixpssmapg  8878  enrefnn  8995  pw2f1olem  9021  domsdomtr  9052  xpen  9080  mapen  9081  mapdom1  9082  phplem2  9141  mapfienlem1  9320  elfir  9330  wdomen2  9494  carden2b  9891  harcard  9902  isinffi  9916  acnlem  9970  acndom  9973  alephdom  10003  fin23lem21  10261  fin23lem39  10272  isf32lem5  10279  fin1a2lem12  10333  axdc3lem2  10373  ttukeylem1  10431  pwcfsdom  10506  canthp1  10577  nqereu  10852  addpqf  10867  axmulf  11069  axmulass  11080  axdistr  11081  ltaddnegr  11362  negeu  11382  fimaxre3  12100  nnsub  12201  nn0sub  12463  ltsubnn0  12464  elz2  12518  uzaddcl  12829  qaddcl  12890  xltneg  13144  xleneg  13145  supxrbnd1  13248  infxrgelb  13263  iccneg  13400  uzsubsubfz  13474  fzsplit2  13477  fzadd2  13487  fzss1  13491  uzsplit  13524  fzdif1  13533  fz0fzdiffz0  13565  difelfzle  13569  difelfznle  13570  fvffz0  13574  preduz  13578  predfz  13581  fzonlt0  13610  fzouzsplit  13622  fzo0addelr  13647  eluzgtdifelfzo  13655  elfzodifsumelfzo  13659  ssfzo12  13687  elfznelfzob  13702  fllt  13738  flflp1  13739  uzsup  13795  negmod  13851  modifeq2int  13868  modfzo0difsn  13878  modsumfzodifsn  13879  om2uzlt2i  13886  nn0ennn  13914  suppssfz  13929  seqfveq2  13959  sermono  13969  seqf1o  13978  ser1const  13993  rpexpmord  14103  mulsubdivbinom2  14197  faclbnd  14225  bcval4  14242  bcpasc  14256  hashkf  14267  hashunx  14321  fz1isolem  14396  ishashinf  14398  seqcoll  14399  ccatval1  14512  ccatval21sw  14521  ccatrn  14525  ccatalpha  14529  swrdnd0  14593  swrd0  14594  swrdfv2  14597  swrdspsleq  14601  addlenpfx  14626  ccatpfx  14636  swrdswrd  14640  pfxccatin12lem2  14666  pfxccat3  14669  swrdccat  14670  revccat  14701  repswswrd  14719  cshwmodn  14730  cshwidxmod  14738  repswcshw  14747  2cshwid  14749  2cshwcom  14751  2cshwcshw  14760  cshwcshid  14762  cshwcsh2id  14763  s1co  14768  cshco  14771  trclub  14933  shftfval  15005  seqshft  15020  crim  15050  caubnd  15294  limsuplt  15414  isercolllem2  15601  fsumcvg  15647  fsumcvg2  15662  fsumshftm  15716  fsumo1  15747  isumshft  15774  harmonic  15794  cvgrat  15818  mertenslem1  15819  zprod  15872  fprodmodd  15932  bpolylem  15983  bpolysum  15988  bpolydiflem  15989  fsumkthpow  15991  rpnnen2lem12  16162  dvdsval3  16195  negdvdsb  16211  dvdsnegb  16212  dvdsmul1  16216  dvdsabseq  16252  dvdsssfz1  16257  odd2np1  16280  divalglem8  16339  ndvdsadd  16349  dfgcd2  16485  dvdssqim  16493  nn0seqcvgd  16509  seq1st  16510  algcvgblem  16516  lcmf  16572  lcmfunsnlem2  16579  cncongr2  16607  prmdvdsfz  16644  isprm7  16647  prmndvdsfaclt  16664  powm2modprm  16743  modprm0  16745  modprmn0modprm0  16747  pythagtriplem1  16756  pythagtriplem4  16759  pythagtriplem8  16763  pythagtriplem9  16764  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  pcexp  16799  pc2dvds  16819  pcz  16821  fldivp1  16837  pcfac  16839  oddprmdvds  16843  pockthg  16846  infpnlem1  16850  prmreclem1  16856  prmreclem2  16857  1arith  16867  4sqlem11  16895  vdwlem2  16922  vdwlem8  16928  vdwnnlem2  16936  prmgaplem7  16997  prmgaplem8  16998  cshwshashlem2  17036  cshwshashlem3  17037  pwsval  17418  isacs1i  17592  funcsetcestrclem9  18098  ismgmid  18602  mgmhmpropd  18635  mhmpropd  18729  smndex1gid  18840  smndex1id  18848  grpsubid1  18967  mulgnnp1  19024  mulgsubcl  19030  mulgnn0z  19043  mulgnndir  19045  mulgneg2  19050  lagsubg  19136  ghmco  19177  symg2bas  19334  symgextfv  19359  pgpfi2  19547  efgsfo  19680  frgpupf  19714  frgpup1  19716  gsummptshft  19877  telgsumfzslem  19929  telgsums  19934  ablfac1eu  20016  pgpfac1lem2  20018  ablfaclem3  20030  dvdsrid  20315  dvdsrneg  20318  dvr1  20355  abv1  20770  lmodfopne  20863  lbsexg  21131  xrsds  21376  znf1o  21518  lindfmm  21794  gsummoncoe1  22264  matecl  22381  mavmul0g  22509  gsummatr01  22615  mp2pm2mplem4  22765  chfacfisf  22810  chfacfisfcpmat  22811  chfacfpmmulgsum2  22821  cpmadugsumlemF  22832  isclo  23043  resttopon  23117  restcld  23128  restcls  23137  iscn  23191  iscnp  23193  cnco  23222  cndis  23247  cnindis  23248  cmpsub  23356  hauscmplem  23362  cmpfii  23365  ptcnplem  23577  txtube  23596  txcmplem1  23597  xkoptsub  23610  qtoptop  23656  kqfval  23679  hmeoco  23728  fileln0  23806  trfil1  23842  trfil2  23843  trufil  23866  elfm3  23906  hausflf2  23954  isucn  24233  bl2in  24356  metss2lem  24467  metss2  24468  stdbdxmet  24471  metrest  24480  nmval2  24548  nmoix  24685  ioo2bl  24749  xrsxmet  24766  expcn  24831  expcnOLD  24833  elcncf  24850  icccvx  24916  cphsscph  25219  iscmet3  25261  causs  25266  metcld2  25275  metsscmetcld  25283  cncmet  25290  bcth3  25299  ovolgelb  25449  ovolfi  25463  shft2rab  25477  uniioombllem3  25554  dyadmax  25567  dyadmbl  25569  subopnmbl  25573  volcn  25575  mbfid  25604  mbfeqalem2  25611  mbfres  25613  cnmbf  25628  i1fmulc  25672  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  itg2seq  25711  itg2gt0  25729  itgss3  25784  dvexp  25925  plypow  26178  plyeq0lem  26183  coeidlem  26210  dgrlt  26240  dgrcolem2  26248  elqaalem2  26296  aacjcl  26303  aaliou3lem1  26318  aaliou3lem2  26319  pserdvlem2  26406  abelthlem8  26417  cosord  26508  sinord  26511  resinf1o  26513  relogexp  26573  logdivlt  26598  advlogexp  26632  logcxp  26646  cxpcl  26651  rpcxpcl  26653  cxpne0  26654  logbchbase  26749  logbgt0b  26771  birthdaylem2  26930  cxplim  26950  divsqrtsumo1  26962  zetacvg  26993  wilthlem1  27046  ftalem7  27057  basellem1  27059  issqf  27114  sqf11  27117  sgmf  27123  sgmnncl  27125  sqff1o  27160  dvdsflsumcom  27166  mpodvdsmulf1o  27172  dvdsmulf1o  27174  sgmppw  27176  chtublem  27190  chtub  27191  logexprlim  27204  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgsdirnn0  27323  gausslemma2dlem1a  27344  gausslemma2dlem5a  27349  lgsquad2  27365  lgsquad3  27366  2sqreulem1  27425  2sqreunnlem1  27428  dchrisumlem1  27468  dchrisumlem2  27469  dchrisumlem3  27470  mulogsumlem  27510  noextenddif  27648  addsrid  27972  ltnegs  28053  lenegs  28054  om2noseqlt2  28308  elzn0s  28406  eln0zs  28408  peano5uzs  28412  bdayfinbndlem1  28475  brbtwn  28984  uspgrupgrushgr  29264  usgrumgruspgr  29267  cusgrfilem2  29542  finsumvtxdg2ssteplem2  29632  cyclnumvtx  29885  crctcshwlkn0lem4  29898  crctcshwlkn0lem6  29900  crctcshwlkn0lem7  29901  crctcshwlkn0  29906  elwspths2spth  30055  rusgrnumwwlk  30063  clwlkclwwlklem2fv2  30083  erclwwlknref  30156  1to2vfriswmgr  30366  4cycl2v2nb  30376  frgr2wwlkeqm  30418  nvo00  30848  nmorepnf  30855  ubthlem1  30957  normpyc  31233  occon3  31384  pjpreeq  31485  idcnop  32068  riesz3i  32149  cnlnssadj  32167  rnbra  32194  strlem3a  32339  cvcon3  32371  ssdmd1  32400  ssdmd2  32401  relfi  32688  fcobijfs2  32811  fzsplit3  32883  prmsimpcyc  33321  esumcst  34240  dmvlsiga  34306  ballotlemimin  34683  bnj545  35070  bnj929  35111  bnj953  35114  fineqvnttrclselem1  35296  pthhashvtx  35341  derangsn  35383  iscvm  35472  cvmsval  35479  cvmliftlem7  35504  cvmlift2lem12  35527  mclsssvlem  35775  supfz  35942  faclimlem3  35958  opnrebl2  36534  nn0prpwlem  36535  tailval  36586  nndivlub  36671  ctbssinf  37650  finixpnum  37845  ltflcei  37848  lindsdom  37854  lindsenlbs  37855  matunitlindflem2  37857  poimirlem4  37864  poimirlem14  37874  poimirlem15  37875  poimirlem19  37879  poimirlem20  37880  poimirlem22  37882  poimirlem24  37884  poimirlem28  37888  poimirlem30  37890  poimirlem31  37891  mblfinlem2  37898  mblfinlem3  37899  mblfinlem4  37900  ftc1anclem1  37933  ftc1anclem4  37936  ftc1anclem5  37937  ftc1anclem7  37939  ftc1anclem8  37940  ftc1anc  37941  caushft  38001  ismtyval  38040  heiborlem7  38057  heiborlem10  38060  heibor  38061  lcmineqlem8  42395  deg1gprod  42499  f1o2d2  42594  oexpreposd  42681  elrfirn  43041  ismrc  43047  nacsfix  43058  mzpcompact2lem  43097  eldiophb  43103  ellz1  43113  rexrabdioph  43140  congrep  43319  jm2.26a  43346  rngunsnply  43515  mendring  43534  iocmbl  43559  oeord2lim  43655  cantnfresb  43670  omabs2  43678  ofoafg  43700  dfno2  43773  rp-isfinite5  43862  enrelmap  44342  expgrowthi  44678  cnfex  45377  xlimclim2lem  46186  climxlim2  46193  icccncfext  46234  itgsinexp  46302  iblspltprt  46320  itgspltprt  46326  fourierdlem50  46503  fourierswlem  46577  etransclem35  46616  zm1nn  47651  subsubelfzo0  47675  ceilbi  47682  addmodne  47693  m1modmmod  47707  modlt0b  47712  iccpartres  47767  iccelpart  47782  iccpartiun  47783  iccpartnel  47787  goldbachthlem1  47894  goldbachth  47896  odz2prm2pw  47912  2pwp1prm  47938  evenltle  48066  fpprwpprb  48089  sbgoldbaltlem2  48129  bgoldbachlt  48162  isubgredg  48215  gricushgr  48266  uhgrimisgrgriclem  48279  gpgvtx0  48402  gpg5nbgrvtx13starlem2  48421  upgrwlkupwlk  48489  2zrngamgm  48594  lincresunit3  48830  lincreslvec3  48831  isldepslvec2  48834  blengt1fldiv2p1  48942  dignn0flhalf  48967  nn0sumshdiglemA  48968  rrx2pnedifcoorneor  49065  precofval2  49717  aacllem  50149