Theorem syl2an2r 681

Description: syl2anr 595 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 578	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 589	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  disjxiun  5144  axprlem4  5423  brcogw  5867  funfni  6654  f1un  6852  fvelimab  6963  dff3  7100  fnex  7220  f1cofveqaeq  7259  f1eqcocnv  7301  f1eqcocnvOLD  7302  caofid0l  7703  caofid0r  7704  caofid1  7705  caofid2  7706  onmindif2  7797  limsssuc  7841  fnse  8121  frrlem13  8285  iinon  8342  smoord  8367  smoword  8368  tfrlem11  8390  coflton  8672  cofonr  8675  naddasslem2  8696  boxcutc  8937  f1domg  8970  phpeqd  9217  phpeqdOLD  9227  ominf  9260  f1finf1o  9273  findcard3OLD  9288  unfilem1  9312  f1opwfi  9358  marypha2  9436  supmax  9464  infmin  9491  ordtypelem6  9520  oiexg  9532  oien  9535  cantnff  9671  cantnfp1lem3  9677  cantnflem1b  9683  cantnflem1  9686  ttrcltr  9713  ttrclselem2  9723  opwf  9809  rankopb  9849  xpnum  9948  infxpenlem  10010  infxp  10212  cflim2  10260  cofsmo  10266  cfsmolem  10267  cfcoflem  10269  ssfin3ds  10327  isf34lem5  10375  isf34lem6  10377  isfin1-3  10383  axcc3  10435  alephval2  10569  fpwwe2lem7  10634  canthp1  10651  tsken  10751  ltaddpr  11031  dedekind  11381  recextlem2  11849  recex  11850  gt0div  12084  ge0div  12085  lerec2  12106  uzwo2  12900  infssuzcl  12920  qmulcl  12955  xnegdi  13231  xmulpnf1n  13261  xadddi2  13280  fzm1  13585  2submod  13901  addmodlteq  13915  expnlbnd  14200  faclbnd5  14262  hasheni  14312  hashdifpr  14379  hashgt23el  14388  ccatrn  14543  ccatalpha  14547  swrds1  14620  swrdccat2  14623  ccatpfx  14655  swrdccatin2  14683  pfxccatin12lem2  14685  revccat  14720  revrev  14721  swrdco  14792  relexpindlem  15014  resqrex  15201  fzomaxdiflem  15293  climconst  15491  serf0  15631  fsumf1o  15673  fsumrev  15729  fsumabs  15751  cvgcmp  15766  binomlem  15779  isumshft  15789  climcndslem1  15799  climcndslem2  15800  climcnds  15801  supcvg  15806  fprodcl2lem  15898  tanneg  16095  rpnnen2lem11  16171  modm1div  16213  fzo0dvdseq  16270  bitsfzolem  16379  gcdcllem3  16446  hashdvds  16712  prmdivdiv  16724  reumodprminv  16741  nnnn0modprm0  16743  pythagtrip  16771  dvdsprmpweqle  16823  pockthg  16843  4sqlem9  16883  vdwmc2  16916  vdwlem2  16919  imasaddflem  17480  acsfn1  17609  acsfn1c  17610  acsfn2  17611  oppccofval  17665  rescabs  17786  diag2  18202  grprinvlem  18598  issubmnd  18686  imasmnd  18697  pwsco2mhm  18750  gsumwspan  18763  frmdss2  18780  grpinvssd  18936  pwssub  18973  imasgrp  18975  subginv  19049  subginvcl  19051  ecqusaddcl  19108  ghmpreima  19152  conjnsg  19168  gass  19206  gsmsymgreqlem2  19340  f1omvdmvd  19352  symgsssg  19376  symgfisg  19377  symgtrinv  19381  psgnunilem5  19403  sylow1lem2  19508  odcau  19513  sylow2a  19528  sylow2  19535  efgsp1  19646  frgpuptf  19679  frgpuptinv  19680  frgpupf  19682  frgpup3lem  19686  mulgdi  19735  gsumval3eu  19813  gsumzsplit  19836  gsumzmhm  19846  gsumxp2  19889  prdsgsum  19890  fsfnn0gsumfsffz  19892  ablfaclem3  19998  srgbinomlem  20124  gsummgp0  20206  imasring  20218  dvdsr01  20262  rngisom1  20357  01eq0ring  20419  issubrng2  20446  subrgcrng  20465  subrginv  20478  isdrngd  20533  imadrhmcl  20556  abv1z  20583  lcomfsupp  20656  lmodvneg1  20659  lspsn  20757  lmhmco  20798  lmhmima  20802  lmhmpreima  20803  reslmhm  20807  lbsextlem2  20917  lidl0cl  20984  2idlcpblrng  21020  quscrng  21029  isridlrng  21031  rnglidlmmgm  21034  rnglidlmsgrp  21035  rngqiprngghmlem1  21046  rngqiprngghmlem3  21048  rngqiprnglinlem3  21052  rngqiprngimf1lem  21053  rngqiprngimf  21056  rng2idl1cntr  21064  znfld  21335  ipassr2  21419  ocvin  21446  pjfo  21489  obsne0  21499  frlmgsum  21546  aspval2  21671  psrlinv  21735  mplsubglem  21777  mpllsslem  21778  evlslem4  21856  evlslem1  21864  mpfind  21889  evls1rhm  22061  madetsumid  22183  scmatcrng  22243  mdetleib2  22310  cramerimplem1  22405  m2pmfzgsumcl  22470  decpmatmul  22494  pmatcollpwscmat  22513  idpm2idmp  22523  pm2mpmhmlem1  22540  chpscmatgsummon  22567  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  topbas  22695  uncld  22765  incld  22767  elcls  22797  neiptopnei  22856  resttopon  22885  restdis  22902  cnclima  22992  paste  23018  cncmp  23116  clsconn  23154  conncompcld  23158  1stcfb  23169  2ndcsb  23173  2ndcredom  23174  kgencmp2  23270  txss12  23329  qtoptop2  23423  qtoptopon  23428  hmphindis  23521  uffixfr  23647  ufildr  23655  isfcls2  23737  tgplacthmeo  23827  tsmsgsum  23863  tgptsmscld  23875  tsmssplit  23876  ustuqtop5  23970  uspreg  23999  prdsxmetlem  24094  prdsbl  24220  metss  24237  metrest  24253  nrmmetd  24303  isngp2  24326  ngpsubcan  24343  lssnlm  24438  nmoid  24479  opnreen  24567  mpomulcn  24605  evth  24705  htpyco2  24725  phtpyco2  24736  clmvz  24858  tcphcph  24985  iscmet3  25041  metcld  25054  bcthlem2  25073  cssbn  25123  chlcsschl  25126  minveclem1  25172  evthicc2  25209  ovolunlem1a  25245  ovolicc2lem1  25266  ovolicc2lem4  25269  ovolicc2lem5  25270  uniioombllem2  25332  uniioombllem3  25334  vitalilem2  25358  vitalilem4  25360  vitalilem5  25361  itg2monolem1  25500  cpnres  25687  rolle  25742  dvlip2  25747  dvivthlem2  25761  dvfsumrlimge0  25782  deg1pwle  25872  plydivlem4  26045  ulm0  26139  efif1olem1  26287  efif1olem2  26288  eflogeq  26346  argimlt0  26357  logrec  26504  relogbcxp  26526  atanlogadd  26655  atanlogsub  26657  atantan  26664  ftalem4  26816  ftalem5  26817  basellem3  26823  chtub  26951  dchrpt  27006  dchrsum2  27007  gausslemma2dlem1a  27104  2lgslem3a1  27139  2lgslem3b1  27140  2lgslem3c1  27141  2lgslem3d1  27142  2lgsoddprm  27155  dchrisumlem2  27229  pntrsumbnd2  27306  nosupbnd1lem4  27450  noinfbnd2lem1  27469  scutbdaylt  27556  oldlim  27618  madebday  27631  cofcutr  27649  negsbdaylem  27769  cnvmot  28059  tglineneq  28162  midexlem  28210  midex  28255  axlowdimlem14  28480  uhgrspansubgrlem  28814  usgrres  28832  usgrnbcnvfv  28889  finsumvtxdg2sstep  29073  uspgr2wlkeq  29170  redwlk  29196  pthdivtx  29253  usgr2wlkspthlem2  29282  wwlknvtx  29366  2wlkdlem6  29452  umgr2wlkon  29471  rusgrnumwwlk  29496  clwwlkwwlksb  29574  clwwlknwwlksnb  29575  clwwnisshclwwsn  29579  clwwlknscsh  29582  clwlknf1oclwwlknlem1  29601  1wlkdlem2  29658  fusgreghash2wsp  29858  2clwwlklem  29863  2clwwlk2clwwlk  29870  numclwwlk6  29910  ofrn2  32132  ofpreima2  32158  wrdsplex  32371  ccatf1  32382  mgcf1o  32440  gsumhashmul  32478  cycpmco2lem5  32559  cycpmco2lem6  32560  cycpmco2lem7  32561  cycpmco2  32562  cyc3co2  32569  imaslmod  32738  rspsnel  32758  elrspunidl  32820  qsidomlem1  32845  qsidomlem2  32846  dimpropd  32981  lbsdiflsp0  32999  extdg1id  33030  zarcmplem  33159  eulerpartlemgvv  33673  pfxwlk  34412  revwlk  34413  pthhashvtx  34416  spthcycl  34418  umgracycusgr  34443  subfacp1lem5  34473  satfvsucsuc  34654  cnambfre  36839  frlmvscadiccat  41386  ricdrng1  41406  pwsgprod  41416  evlsval3  41433  evlsbagval  41440  0prjspn  41672  3cubes  41730  oninfint  42287  onexomgt  42292  onexoegt  42295  ordeldif  42310  oacl2g  42382  onmcl  42383  omabs2  42384  omcl2  42385  tfsconcatfv  42393  tfsconcatrev  42400  ofoafg  42406  ofoafo  42408  ofoaass  42412  ofoacom  42413  onsucunifi  42422  oaun3lem1  42426  oadif1lem  42431  oadif1  42432  naddwordnexlem4  42454  safesnsupfilb  42471  gneispace  43187  rr-phpd  43264  grumnudlem  43346  ax6e2ndeqALT  43994  sineq0ALT  44000  fnresdmss  44165  saliinclf  45340  setsv  46344  sprsymrelfolem2  46459  lighneal  46577  isomuspgrlem2c  46796  lincresunit3  47249  2itscp  47554