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  5144  axprlem4OLD  5434  brcogw  5881  funfni  6674  f1un  6868  fvelimab  6980  dff3  7119  fnex  7236  ralima  7256  f1cofveqaeq  7277  f1eqcocnv  7320  caofid0l  7729  caofid0r  7730  caofid1  7731  caofid2  7732  onmindif2  7826  limsssuc  7870  mptcnfimad  8009  fnse  8156  frrlem13  8321  iinon  8378  smoord  8403  smoword  8404  tfrlem11  8426  coflton  8707  cofonr  8710  naddasslem2  8731  boxcutc  8979  f1domg  9010  phpeqd  9249  phpeqdOLD  9259  ominf  9291  f1finf1o  9302  findcard3OLD  9316  unfilem1  9340  f1opwfi  9393  marypha2  9476  supmax  9504  infmin  9531  ordtypelem6  9560  oiexg  9572  oien  9575  cantnff  9711  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1  9726  ttrcltr  9753  ttrclselem2  9763  opwf  9849  rankopb  9889  xpnum  9988  infxpenlem  10050  infxp  10251  cflim2  10300  cofsmo  10306  cfsmolem  10307  cfcoflem  10309  ssfin3ds  10367  isf34lem5  10415  isf34lem6  10417  isfin1-3  10423  axcc3  10475  alephval2  10609  fpwwe2lem7  10674  canthp1  10691  tsken  10791  ltaddpr  11071  dedekind  11421  recextlem2  11891  recex  11892  gt0div  12131  ge0div  12132  lerec2  12153  uzwo2  12951  infssuzcl  12971  qmulcl  13006  xnegdi  13286  xmulpnf1n  13316  xadddi2  13335  fzm1  13643  2submod  13969  addmodlteq  13983  expnlbnd  14268  faclbnd5  14333  hasheni  14383  hashdifpr  14450  hashgt23el  14459  ccatrn  14623  ccatalpha  14627  swrds1  14700  swrdccat2  14703  ccatpfx  14735  swrdccatin2  14763  pfxccatin12lem2  14765  revccat  14800  revrev  14801  swrdco  14872  relexpindlem  15098  resqrex  15285  fzomaxdiflem  15377  climconst  15575  serf0  15713  fsumf1o  15755  fsumrev  15811  fsumabs  15833  cvgcmp  15848  binomlem  15861  isumshft  15871  climcndslem1  15881  climcndslem2  15882  climcnds  15883  supcvg  15888  fprodcl2lem  15982  tanneg  16180  rpnnen2lem11  16256  modm1div  16298  fzo0dvdseq  16356  bitsfzolem  16467  gcdcllem3  16534  hashdvds  16808  prmdivdiv  16820  reumodprminv  16837  nnnn0modprm0  16839  pythagtrip  16867  dvdsprmpweqle  16919  pockthg  16939  4sqlem9  16979  vdwmc2  17012  vdwlem2  17015  imasaddflem  17576  acsfn1  17705  acsfn1c  17706  acsfn2  17707  oppccofval  17761  rescabs  17882  diag2  18301  grpinvalem  18698  issubmnd  18786  imasmnd  18800  pwsco2mhm  18858  gsumwspan  18871  frmdss2  18888  grpinvssd  19047  pwssub  19084  imasgrp  19086  subginv  19163  subginvcl  19165  ecqusaddcl  19223  ghmpreima  19268  conjnsg  19284  gass  19331  gsmsymgreqlem2  19463  f1omvdmvd  19475  symgsssg  19499  symgfisg  19500  symgtrinv  19504  psgnunilem5  19526  sylow1lem2  19631  odcau  19636  sylow2a  19651  sylow2  19658  efgsp1  19769  frgpuptf  19802  frgpuptinv  19803  frgpupf  19805  frgpup3lem  19809  mulgdi  19858  gsumval3eu  19936  gsumzsplit  19959  gsumzmhm  19969  gsumxp2  20012  prdsgsum  20013  fsfnn0gsumfsffz  20015  ablfaclem3  20121  srgbinomlem  20247  gsummgp0  20331  imasring  20343  dvdsr01  20387  rngisom1  20482  01eq0ring  20546  issubrng2  20574  subrgcrng  20591  subrginv  20604  isdrngd  20781  imadrhmcl  20814  abv1z  20841  lcomfsupp  20916  lmodvneg1  20919  lspsn  21017  lmhmco  21059  lmhmima  21063  lmhmpreima  21064  reslmhm  21068  lbsextlem2  21178  isridlrng  21246  lidl0cl  21247  elrspsn  21267  rnglidlmmgm  21272  rnglidlmsgrp  21273  2idlcpblrng  21298  quscrng  21310  rngqiprngghmlem1  21314  rngqiprngghmlem3  21316  rngqiprnglinlem3  21320  rngqiprngimf1lem  21321  rngqiprngimf  21324  rng2idl1cntr  21332  znfld  21596  ipassr2  21682  ocvin  21709  pjfo  21752  obsne0  21762  frlmgsum  21809  aspval2  21935  psrlinv  21992  mplsubglem  22036  mpllsslem  22037  evlslem4  22117  evlslem1  22123  mpfind  22148  evls1rhm  22341  madetsumid  22482  scmatcrng  22542  mdetleib2  22609  cramerimplem1  22704  m2pmfzgsumcl  22769  decpmatmul  22793  pmatcollpwscmat  22812  idpm2idmp  22822  pm2mpmhmlem1  22839  chpscmatgsummon  22866  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  topbas  22994  uncld  23064  incld  23066  elcls  23096  neiptopnei  23155  resttopon  23184  restdis  23201  cnclima  23291  paste  23317  cncmp  23415  clsconn  23453  conncompcld  23457  1stcfb  23468  2ndcsb  23472  2ndcredom  23473  kgencmp2  23569  txss12  23628  qtoptop2  23722  qtoptopon  23727  hmphindis  23820  uffixfr  23946  ufildr  23954  isfcls2  24036  tgplacthmeo  24126  tsmsgsum  24162  tgptsmscld  24174  tsmssplit  24175  ustuqtop5  24269  uspreg  24298  prdsxmetlem  24393  prdsbl  24519  metss  24536  metrest  24552  nrmmetd  24602  isngp2  24625  ngpsubcan  24642  lssnlm  24737  nmoid  24778  opnreen  24866  mpomulcn  24904  evth  25004  htpyco2  25024  phtpyco2  25035  clmvz  25157  tcphcph  25284  iscmet3  25340  metcld  25353  bcthlem2  25372  cssbn  25422  chlcsschl  25425  minveclem1  25471  evthicc2  25508  ovolunlem1a  25544  ovolicc2lem1  25565  ovolicc2lem4  25568  ovolicc2lem5  25569  uniioombllem2  25631  uniioombllem3  25633  vitalilem2  25657  vitalilem4  25659  vitalilem5  25660  itg2monolem1  25799  cpnres  25987  rolle  26042  dvlip2  26048  dvivthlem2  26062  dvfsumrlimge0  26085  deg1pwle  26173  plydivlem4  26352  ulm0  26448  efif1olem1  26598  efif1olem2  26599  eflogeq  26658  argimlt0  26669  logrec  26820  relogbcxp  26842  atanlogadd  26971  atanlogsub  26973  atantan  26980  ftalem4  27133  ftalem5  27134  basellem3  27140  chtub  27270  dchrpt  27325  dchrsum2  27326  gausslemma2dlem1a  27423  2lgslem3a1  27458  2lgslem3b1  27459  2lgslem3c1  27460  2lgslem3d1  27461  2lgsoddprm  27474  dchrisumlem2  27548  pntrsumbnd2  27625  nosupbnd1lem4  27770  noinfbnd2lem1  27789  scutbdaylt  27877  oldlim  27939  madebday  27952  cofcutr  27972  addsbday  28064  negsbdaylem  28102  absmuls  28282  abssneg  28285  cnvmot  28563  tglineneq  28666  midexlem  28714  midex  28759  axlowdimlem14  28984  uhgrspansubgrlem  29321  usgrres  29339  usgrnbcnvfv  29396  finsumvtxdg2sstep  29581  uspgr2wlkeq  29678  redwlk  29704  pthdivtx  29761  usgr2wlkspthlem2  29790  wwlknvtx  29874  2wlkdlem6  29960  umgr2wlkon  29979  rusgrnumwwlk  30004  clwwlkwwlksb  30082  clwwlknwwlksnb  30083  clwwnisshclwwsn  30087  clwwlknscsh  30090  clwlknf1oclwwlknlem1  30109  1wlkdlem2  30166  fusgreghash2wsp  30366  2clwwlklem  30371  2clwwlk2clwwlk  30378  numclwwlk6  30418  ofrn2  32656  ofpreima2  32682  wrdsplex  32904  ccatf1  32917  mgcf1o  32977  gsumfs2d  33040  gsumhashmul  33046  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  cyc3co2  33142  elrgspnlem1  33231  elrgspnlem2  33232  erler  33251  fracerl  33287  imaslmod  33360  elrspunidl  33435  qsidomlem1  33459  qsidomlem2  33460  ssdifidllem  33463  ssdifidlprm  33465  dimpropd  33635  lbsdiflsp0  33653  extdg1id  33690  fldext2chn  33733  madjusmdetlem2  33788  zarcmplem  33841  eulerpartlemgvv  34357  pfxwlk  35107  revwlk  35108  pthhashvtx  35111  spthcycl  35113  umgracycusgr  35138  subfacp1lem5  35168  satfvsucsuc  35349  ply1divalg3  35626  weiunfrlem  36446  cnambfre  37654  frlmvscadiccat  42492  ricdrng1  42514  pwsgprod  42530  evlsval3  42545  evlsbagval  42552  0prjspn  42614  3cubes  42677  oninfint  43224  onexomgt  43229  onexoegt  43232  ordeldif  43247  oacl2g  43319  onmcl  43320  omabs2  43321  omcl2  43322  tfsconcatfv  43330  tfsconcatrev  43337  ofoafg  43343  ofoafo  43345  ofoaass  43349  ofoacom  43350  onsucunifi  43359  oaun3lem1  43363  oadif1lem  43368  oadif1  43369  naddwordnexlem4  43390  safesnsupfilb  43407  gneispace  44123  rr-phpd  44198  grumnudlem  44280  ax6e2ndeqALT  44928  sineq0ALT  44934  fnresdmss  45110  saliinclf  46281  setsv  47302  sprsymrelfolem2  47417  lighneal  47535  isuspgrim0lem  47808  isuspgrim0  47809  grimuhgr  47815  grimcnv  47816  clnbgrgrim  47839  grimedg  47840  isubgr3stgrlem8  47875  clnbgr3stgrgrlic  47914  lincresunit3  48326  2itscp  48630