Theorem syl2an2r 684

Description: syl2anr 599 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 583	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 594	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:  disjxiun  5029  axprlem4  5295  brcogw  5708  funfni  6439  fvelimab  6725  dff3  6857  fnex  6971  f1cofveqaeq  7008  f1eqcocnv  7049  f1eqcocnvOLD  7050  caofid0l  7435  caofid0r  7436  caofid1  7437  caofid2  7438  onmindif2  7526  limsssuc  7564  fnse  7832  iinon  7987  smoord  8012  smoword  8013  tfrlem11  8034  boxcutc  8523  f1domg  8547  phpeqd  8728  findcard3  8794  unfilem1  8815  f1opwfi  8861  marypha2  8936  supmax  8964  infmin  8991  ordtypelem6  9020  oiexg  9032  oien  9035  cantnff  9170  cantnfp1lem3  9176  cantnflem1b  9182  cantnflem1  9185  opwf  9274  rankopb  9314  xpnum  9413  infxpenlem  9473  infxp  9675  cflim2  9723  cofsmo  9729  cfsmolem  9730  cfcoflem  9732  ssfin3ds  9790  isf34lem5  9838  isf34lem6  9840  isfin1-3  9846  axcc3  9898  alephval2  10032  fpwwe2lem7  10097  canthp1  10114  tsken  10214  ltaddpr  10494  dedekind  10841  recextlem2  11309  recex  11310  gt0div  11544  ge0div  11545  lerec2  11566  uzwo2  12352  infssuzcl  12372  qmulcl  12407  xnegdi  12682  xmulpnf1n  12712  xadddi2  12731  fzm1  13036  2submod  13349  addmodlteq  13363  expnlbnd  13644  faclbnd5  13708  hasheni  13758  hashdifpr  13826  hashgt23el  13835  ccatrn  13990  ccatalpha  13994  swrds1  14075  swrdccat2  14078  ccatpfx  14110  swrdccatin2  14138  pfxccatin12lem2  14140  revccat  14175  revrev  14176  swrdco  14246  relexpindlem  14470  resqrex  14658  fzomaxdiflem  14750  climconst  14948  serf0  15085  fsumf1o  15128  fsumrev  15182  fsumabs  15204  cvgcmp  15219  binomlem  15232  isumshft  15242  climcndslem1  15252  climcndslem2  15253  climcnds  15254  supcvg  15259  fprodcl2lem  15352  tanneg  15549  rpnnen2lem11  15625  modm1div  15667  fzo0dvdseq  15724  bitsfzolem  15833  gcdcllem3  15900  hashdvds  16167  prmdivdiv  16179  reumodprminv  16196  nnnn0modprm0  16198  pythagtrip  16226  dvdsprmpweqle  16277  pockthg  16297  4sqlem9  16337  vdwmc2  16370  vdwlem2  16373  imasaddflem  16861  acsfn1  16990  acsfn1c  16991  acsfn2  16992  oppccofval  17044  diag2  17561  grprinvlem  17949  issubmnd  18004  imasmnd  18015  pwsco2mhm  18063  gsumwspan  18077  frmdss2  18094  grpinvssd  18243  pwssub  18280  imasgrp  18282  subginv  18353  subginvcl  18355  ghmpreima  18447  conjnsg  18461  gass  18498  gsmsymgreqlem2  18626  f1omvdmvd  18638  symgsssg  18662  symgfisg  18663  symgtrinv  18667  psgnunilem5  18689  sylow1lem2  18791  odcau  18796  sylow2a  18811  sylow2  18818  efgsp1  18930  frgpuptf  18963  frgpuptinv  18964  frgpupf  18966  frgpup3lem  18970  mulgdi  19015  gsumval3eu  19092  gsumzsplit  19115  gsumzmhm  19125  gsumxp2  19168  prdsgsum  19169  fsfnn0gsumfsffz  19171  ablfaclem3  19277  srgbinomlem  19362  gsummgp0  19429  imasring  19440  dvdsr01  19476  subrgcrng  19607  subrginv  19619  abv1z  19671  lcomfsupp  19742  lmodvneg1  19745  lspsn  19842  lmhmco  19883  lmhmima  19887  lmhmpreima  19888  reslmhm  19892  lbsextlem2  19999  lidl0cl  20053  znfld  20328  ipassr2  20412  ocvin  20439  pjfo  20480  obsne0  20490  frlmgsum  20537  aspval2  20661  psrlinv  20725  mplsubglem  20764  mpllsslem  20765  evlslem4  20837  evlslem1  20845  mpfind  20870  evls1rhm  21041  madetsumid  21161  scmatcrng  21221  mdetleib2  21288  cramerimplem1  21383  m2pmfzgsumcl  21448  decpmatmul  21472  pmatcollpwscmat  21491  idpm2idmp  21501  pm2mpmhmlem1  21518  chpscmatgsummon  21545  chfacfscmulgsum  21560  chfacfpmmulgsum  21564  topbas  21672  uncld  21741  incld  21743  elcls  21773  neiptopnei  21832  resttopon  21861  restdis  21878  cnclima  21968  paste  21994  cncmp  22092  clsconn  22130  conncompcld  22134  1stcfb  22145  2ndcsb  22149  2ndcredom  22150  kgencmp2  22246  txss12  22305  qtoptop2  22399  qtoptopon  22404  hmphindis  22497  uffixfr  22623  ufildr  22631  isfcls2  22713  tgplacthmeo  22803  tsmsgsum  22839  tgptsmscld  22851  tsmssplit  22852  ustuqtop5  22946  uspreg  22975  prdsxmetlem  23070  prdsbl  23193  metss  23210  metrest  23226  nrmmetd  23276  isngp2  23299  ngpsubcan  23316  lssnlm  23403  nmoid  23444  opnreen  23532  evth  23660  htpyco2  23680  phtpyco2  23691  clmvz  23812  tcphcph  23937  iscmet3  23993  metcld  24006  bcthlem2  24025  cssbn  24075  chlcsschl  24078  minveclem1  24124  evthicc2  24160  ovolunlem1a  24196  ovolicc2lem1  24217  ovolicc2lem4  24220  ovolicc2lem5  24221  uniioombllem2  24283  uniioombllem3  24285  vitalilem2  24309  vitalilem4  24311  vitalilem5  24312  itg2monolem1  24450  cpnres  24636  rolle  24689  dvlip2  24694  dvivthlem2  24708  dvfsumrlimge0  24729  deg1pwle  24819  plydivlem4  24991  ulm0  25085  efif1olem1  25233  efif1olem2  25234  eflogeq  25292  argimlt0  25303  logrec  25448  relogbcxp  25470  atanlogadd  25599  atanlogsub  25601  atantan  25608  ftalem4  25760  ftalem5  25761  basellem3  25767  chtub  25895  dchrpt  25950  dchrsum2  25951  gausslemma2dlem1a  26048  2lgslem3a1  26083  2lgslem3b1  26084  2lgslem3c1  26085  2lgslem3d1  26086  2lgsoddprm  26099  dchrisumlem2  26173  pntrsumbnd2  26250  cnvmot  26434  tglineneq  26537  midexlem  26585  midex  26630  axlowdimlem14  26848  uhgrspansubgrlem  27179  usgrres  27197  usgrnbcnvfv  27254  finsumvtxdg2sstep  27438  uspgr2wlkeq  27534  redwlk  27561  pthdivtx  27617  usgr2wlkspthlem2  27646  wwlknvtx  27730  2wlkdlem6  27816  umgr2wlkon  27835  rusgrnumwwlk  27860  clwwlkwwlksb  27938  clwwlknwwlksnb  27939  clwwnisshclwwsn  27943  clwwlknscsh  27946  clwlknf1oclwwlknlem1  27965  1wlkdlem2  28022  fusgreghash2wsp  28222  2clwwlklem  28227  2clwwlk2clwwlk  28234  numclwwlk6  28274  ofrn2  30499  ofpreima2  30527  wrdsplex  30736  ccatf1  30747  mgcf1o  30807  gsumhashmul  30842  cycpmco2lem5  30923  cycpmco2lem6  30924  cycpmco2lem7  30925  cycpmco2  30926  cyc3co2  30933  imaslmod  31074  rspsnel  31088  elrspunidl  31127  qsidomlem1  31149  qsidomlem2  31150  dimpropd  31213  lbsdiflsp0  31228  extdg1id  31259  zarcmplem  31352  eulerpartlemgvv  31862  pfxwlk  32601  revwlk  32602  pthhashvtx  32605  spthcycl  32607  umgracycusgr  32632  subfacp1lem5  32662  satfvsucsuc  32843  frrlem13  33396  nosupbnd1lem4  33479  noinfbnd2lem1  33498  scutbdaylt  33573  oldlim  33626  cnambfre  35385  frlmvscadiccat  39744  pwsgprod  39776  evlsval3  39777  evlsbagval  39780  0prjspn  39962  3cubes  40004  gneispace  41210  rr-phpd  41289  grumnudlem  41366  ax6e2ndeqALT  42010  sineq0ALT  42016  fnresdmss  42163  setsv  44263  sprsymrelfolem2  44378  lighneal  44496  isomuspgrlem2c  44715  lincresunit3  45255  2itscp  45560