Theorem syl2an2r 685

Description: syl2anr 597 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.)

Hypotheses

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

Assertion

Ref	Expression
syl2an2r	⊢ ((𝜑 ∧ 𝜒) → 𝜏)

Proof of Theorem syl2an2r

Step	Hyp	Ref	Expression
1		syl2an2r.2	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2		syl2an2r.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl2an2r.3	. . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
4	2, 3	sylan 580	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 591	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:  disjxiun  5140  axprlem4OLD  5429  brcogw  5879  funfni  6674  f1un  6868  fvelimab  6981  dff3  7120  fnex  7237  ralima  7257  f1cofveqaeq  7278  f1eqcocnv  7321  caofid0l  7730  caofid0r  7731  caofid1  7732  caofid2  7733  onmindif2  7827  limsssuc  7871  mptcnfimad  8011  fnse  8158  frrlem13  8323  iinon  8380  smoord  8405  smoword  8406  tfrlem11  8428  coflton  8709  cofonr  8712  naddasslem2  8733  boxcutc  8981  f1domg  9012  phpeqd  9252  phpeqdOLD  9262  ominf  9294  f1finf1o  9305  findcard3OLD  9319  unfilem1  9343  f1opwfi  9396  marypha2  9479  supmax  9507  infmin  9534  ordtypelem6  9563  oiexg  9575  oien  9578  cantnff  9714  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  ttrcltr  9756  ttrclselem2  9766  opwf  9852  rankopb  9892  xpnum  9991  infxpenlem  10053  infxp  10254  cflim2  10303  cofsmo  10309  cfsmolem  10310  cfcoflem  10312  ssfin3ds  10370  isf34lem5  10418  isf34lem6  10420  isfin1-3  10426  axcc3  10478  alephval2  10612  fpwwe2lem7  10677  canthp1  10694  tsken  10794  ltaddpr  11074  dedekind  11424  recextlem2  11894  recex  11895  gt0div  12134  ge0div  12135  lerec2  12156  uzwo2  12954  infssuzcl  12974  qmulcl  13009  xnegdi  13290  xmulpnf1n  13320  xadddi2  13339  fzm1  13647  2submod  13973  addmodlteq  13987  expnlbnd  14272  faclbnd5  14337  hasheni  14387  hashdifpr  14454  hashgt23el  14463  ccatrn  14627  ccatalpha  14631  swrds1  14704  swrdccat2  14707  ccatpfx  14739  swrdccatin2  14767  pfxccatin12lem2  14769  revccat  14804  revrev  14805  swrdco  14876  relexpindlem  15102  resqrex  15289  fzomaxdiflem  15381  climconst  15579  serf0  15717  fsumf1o  15759  fsumrev  15815  fsumabs  15837  cvgcmp  15852  binomlem  15865  isumshft  15875  climcndslem1  15885  climcndslem2  15886  climcnds  15887  supcvg  15892  fprodcl2lem  15986  tanneg  16184  rpnnen2lem11  16260  modm1div  16302  fzo0dvdseq  16360  bitsfzolem  16471  gcdcllem3  16538  hashdvds  16812  prmdivdiv  16824  reumodprminv  16842  nnnn0modprm0  16844  pythagtrip  16872  dvdsprmpweqle  16924  pockthg  16944  4sqlem9  16984  vdwmc2  17017  vdwlem2  17020  imasaddflem  17575  acsfn1  17704  acsfn1c  17705  acsfn2  17706  oppccofval  17759  rescabs  17877  diag2  18290  grpinvalem  18686  issubmnd  18774  imasmnd  18788  pwsco2mhm  18846  gsumwspan  18859  frmdss2  18876  grpinvssd  19035  pwssub  19072  imasgrp  19074  subginv  19151  subginvcl  19153  ecqusaddcl  19211  ghmpreima  19256  conjnsg  19272  gass  19319  gsmsymgreqlem2  19449  f1omvdmvd  19461  symgsssg  19485  symgfisg  19486  symgtrinv  19490  psgnunilem5  19512  sylow1lem2  19617  odcau  19622  sylow2a  19637  sylow2  19644  efgsp1  19755  frgpuptf  19788  frgpuptinv  19789  frgpupf  19791  frgpup3lem  19795  mulgdi  19844  gsumval3eu  19922  gsumzsplit  19945  gsumzmhm  19955  gsumxp2  19998  prdsgsum  19999  fsfnn0gsumfsffz  20001  ablfaclem3  20107  srgbinomlem  20227  gsummgp0  20315  imasring  20327  dvdsr01  20371  rngisom1  20466  01eq0ring  20530  issubrng2  20558  subrgcrng  20575  subrginv  20588  isdrngd  20765  imadrhmcl  20798  abv1z  20825  lcomfsupp  20900  lmodvneg1  20903  lspsn  21000  lmhmco  21042  lmhmima  21046  lmhmpreima  21047  reslmhm  21051  lbsextlem2  21161  isridlrng  21229  lidl0cl  21230  elrspsn  21250  rnglidlmmgm  21255  rnglidlmsgrp  21256  2idlcpblrng  21281  quscrng  21293  rngqiprngghmlem1  21297  rngqiprngghmlem3  21299  rngqiprnglinlem3  21303  rngqiprngimf1lem  21304  rngqiprngimf  21307  rng2idl1cntr  21315  znfld  21579  ipassr2  21665  ocvin  21692  pjfo  21735  obsne0  21745  frlmgsum  21792  aspval2  21918  psrlinv  21975  mplsubglem  22019  mpllsslem  22020  evlslem4  22100  evlslem1  22106  mpfind  22131  evls1rhm  22326  madetsumid  22467  scmatcrng  22527  mdetleib2  22594  cramerimplem1  22689  m2pmfzgsumcl  22754  decpmatmul  22778  pmatcollpwscmat  22797  idpm2idmp  22807  pm2mpmhmlem1  22824  chpscmatgsummon  22851  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  topbas  22979  uncld  23049  incld  23051  elcls  23081  neiptopnei  23140  resttopon  23169  restdis  23186  cnclima  23276  paste  23302  cncmp  23400  clsconn  23438  conncompcld  23442  1stcfb  23453  2ndcsb  23457  2ndcredom  23458  kgencmp2  23554  txss12  23613  qtoptop2  23707  qtoptopon  23712  hmphindis  23805  uffixfr  23931  ufildr  23939  isfcls2  24021  tgplacthmeo  24111  tsmsgsum  24147  tgptsmscld  24159  tsmssplit  24160  ustuqtop5  24254  uspreg  24283  prdsxmetlem  24378  prdsbl  24504  metss  24521  metrest  24537  nrmmetd  24587  isngp2  24610  ngpsubcan  24627  lssnlm  24722  nmoid  24763  opnreen  24853  mpomulcn  24891  evth  24991  htpyco2  25011  phtpyco2  25022  clmvz  25144  tcphcph  25271  iscmet3  25327  metcld  25340  bcthlem2  25359  cssbn  25409  chlcsschl  25412  minveclem1  25458  evthicc2  25495  ovolunlem1a  25531  ovolicc2lem1  25552  ovolicc2lem4  25555  ovolicc2lem5  25556  uniioombllem2  25618  uniioombllem3  25620  vitalilem2  25644  vitalilem4  25646  vitalilem5  25647  itg2monolem1  25785  cpnres  25973  rolle  26028  dvlip2  26034  dvivthlem2  26048  dvfsumrlimge0  26071  deg1pwle  26159  plydivlem4  26338  ulm0  26434  efif1olem1  26584  efif1olem2  26585  eflogeq  26644  argimlt0  26655  logrec  26806  relogbcxp  26828  atanlogadd  26957  atanlogsub  26959  atantan  26966  ftalem4  27119  ftalem5  27120  basellem3  27126  chtub  27256  dchrpt  27311  dchrsum2  27312  gausslemma2dlem1a  27409  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgslem3d1  27447  2lgsoddprm  27460  dchrisumlem2  27534  pntrsumbnd2  27611  nosupbnd1lem4  27756  noinfbnd2lem1  27775  scutbdaylt  27863  oldlim  27925  madebday  27938  cofcutr  27958  addsbday  28050  negsbdaylem  28088  absmuls  28268  abssneg  28271  cnvmot  28549  tglineneq  28652  midexlem  28700  midex  28745  axlowdimlem14  28970  uhgrspansubgrlem  29307  usgrres  29325  usgrnbcnvfv  29382  finsumvtxdg2sstep  29567  uspgr2wlkeq  29664  redwlk  29690  pthdivtx  29747  usgr2wlkspthlem2  29778  wwlknvtx  29865  2wlkdlem6  29951  umgr2wlkon  29970  rusgrnumwwlk  29995  clwwlkwwlksb  30073  clwwlknwwlksnb  30074  clwwnisshclwwsn  30078  clwwlknscsh  30081  clwlknf1oclwwlknlem1  30100  1wlkdlem2  30157  fusgreghash2wsp  30357  2clwwlklem  30362  2clwwlk2clwwlk  30369  numclwwlk6  30409  ofrn2  32650  ofpreima2  32676  wrdsplex  32920  ccatf1  32933  mgcf1o  32993  gsumfs2d  33058  gsumhashmul  33064  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  cyc3co2  33160  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnsubrunlem1  33251  erler  33269  fracerl  33308  imaslmod  33381  elrspunidl  33456  qsidomlem1  33480  qsidomlem2  33481  ssdifidllem  33484  ssdifidlprm  33486  exsslsb  33647  dimpropd  33659  lbsdiflsp0  33677  extdg1id  33716  madjusmdetlem2  33827  zarcmplem  33880  eulerpartlemgvv  34378  boolesineq  34457  pfxwlk  35129  revwlk  35130  pthhashvtx  35133  spthcycl  35134  umgracycusgr  35159  subfacp1lem5  35189  satfvsucsuc  35370  ply1divalg3  35647  weiunfrlem  36465  cnambfre  37675  frlmvscadiccat  42516  ricdrng1  42538  pwsgprod  42554  evlsval3  42569  evlsbagval  42576  0prjspn  42638  3cubes  42701  oninfint  43248  onexomgt  43253  onexoegt  43256  ordeldif  43271  oacl2g  43343  onmcl  43344  omabs2  43345  omcl2  43346  tfsconcatfv  43354  tfsconcatrev  43361  ofoafg  43367  ofoafo  43369  ofoaass  43373  ofoacom  43374  onsucunifi  43383  oaun3lem1  43387  oadif1lem  43392  oadif1  43393  naddwordnexlem4  43414  safesnsupfilb  43431  gneispace  44147  rr-phpd  44222  grumnudlem  44304  ax6e2ndeqALT  44951  sineq0ALT  44957  fnresdmss  45173  saliinclf  46341  setsv  47365  sprsymrelfolem2  47480  lighneal  47598  isuspgrim0lem  47871  isuspgrim0  47872  grimuhgr  47878  grimcnv  47879  clnbgrgrim  47902  grimedg  47903  isubgr3stgrlem8  47940  clnbgr3stgrgrlic  47979  lincresunit3  48398  2itscp  48702