Theorem syl2an2r 682

Description: syl2anr 596 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 579	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 590	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 206  df-an 396

This theorem is referenced by:  disjxiun  5145  axprlem4  5424  brcogw  5868  funfni  6655  f1un  6853  fvelimab  6964  dff3  7101  fnex  7221  f1cofveqaeq  7260  f1eqcocnv  7302  f1eqcocnvOLD  7303  caofid0l  7704  caofid0r  7705  caofid1  7706  caofid2  7707  onmindif2  7798  limsssuc  7842  fnse  8122  frrlem13  8286  iinon  8343  smoord  8368  smoword  8369  tfrlem11  8391  coflton  8673  cofonr  8676  naddasslem2  8697  boxcutc  8938  f1domg  8971  phpeqd  9218  phpeqdOLD  9228  ominf  9261  f1finf1o  9274  findcard3OLD  9289  unfilem1  9313  f1opwfi  9359  marypha2  9437  supmax  9465  infmin  9492  ordtypelem6  9521  oiexg  9533  oien  9536  cantnff  9672  cantnfp1lem3  9678  cantnflem1b  9684  cantnflem1  9687  ttrcltr  9714  ttrclselem2  9724  opwf  9810  rankopb  9850  xpnum  9949  infxpenlem  10011  infxp  10213  cflim2  10261  cofsmo  10267  cfsmolem  10268  cfcoflem  10270  ssfin3ds  10328  isf34lem5  10376  isf34lem6  10378  isfin1-3  10384  axcc3  10436  alephval2  10570  fpwwe2lem7  10635  canthp1  10652  tsken  10752  ltaddpr  11032  dedekind  11382  recextlem2  11850  recex  11851  gt0div  12085  ge0div  12086  lerec2  12107  uzwo2  12901  infssuzcl  12921  qmulcl  12956  xnegdi  13232  xmulpnf1n  13262  xadddi2  13281  fzm1  13586  2submod  13902  addmodlteq  13916  expnlbnd  14201  faclbnd5  14263  hasheni  14313  hashdifpr  14380  hashgt23el  14389  ccatrn  14544  ccatalpha  14548  swrds1  14621  swrdccat2  14624  ccatpfx  14656  swrdccatin2  14684  pfxccatin12lem2  14686  revccat  14721  revrev  14722  swrdco  14793  relexpindlem  15015  resqrex  15202  fzomaxdiflem  15294  climconst  15492  serf0  15632  fsumf1o  15674  fsumrev  15730  fsumabs  15752  cvgcmp  15767  binomlem  15780  isumshft  15790  climcndslem1  15800  climcndslem2  15801  climcnds  15802  supcvg  15807  fprodcl2lem  15899  tanneg  16096  rpnnen2lem11  16172  modm1div  16214  fzo0dvdseq  16271  bitsfzolem  16380  gcdcllem3  16447  hashdvds  16713  prmdivdiv  16725  reumodprminv  16742  nnnn0modprm0  16744  pythagtrip  16772  dvdsprmpweqle  16824  pockthg  16844  4sqlem9  16884  vdwmc2  16917  vdwlem2  16920  imasaddflem  17481  acsfn1  17610  acsfn1c  17611  acsfn2  17612  oppccofval  17666  rescabs  17787  diag2  18203  grprinvlem  18599  issubmnd  18687  imasmnd  18698  pwsco2mhm  18751  gsumwspan  18764  frmdss2  18781  grpinvssd  18937  pwssub  18974  imasgrp  18976  subginv  19050  subginvcl  19052  ecqusaddcl  19109  ghmpreima  19153  conjnsg  19169  gass  19207  gsmsymgreqlem2  19341  f1omvdmvd  19353  symgsssg  19377  symgfisg  19378  symgtrinv  19382  psgnunilem5  19404  sylow1lem2  19509  odcau  19514  sylow2a  19529  sylow2  19536  efgsp1  19647  frgpuptf  19680  frgpuptinv  19681  frgpupf  19683  frgpup3lem  19687  mulgdi  19736  gsumval3eu  19814  gsumzsplit  19837  gsumzmhm  19847  gsumxp2  19890  prdsgsum  19891  fsfnn0gsumfsffz  19893  ablfaclem3  19999  srgbinomlem  20125  gsummgp0  20207  imasring  20219  dvdsr01  20263  rngisom1  20358  01eq0ring  20420  issubrng2  20447  subrgcrng  20466  subrginv  20479  isdrngd  20534  imadrhmcl  20557  abv1z  20584  lcomfsupp  20657  lmodvneg1  20660  lspsn  20758  lmhmco  20799  lmhmima  20803  lmhmpreima  20804  reslmhm  20808  lbsextlem2  20918  lidl0cl  20985  2idlcpblrng  21021  quscrng  21030  isridlrng  21032  rnglidlmmgm  21035  rnglidlmsgrp  21036  rngqiprngghmlem1  21047  rngqiprngghmlem3  21049  rngqiprnglinlem3  21053  rngqiprngimf1lem  21054  rngqiprngimf  21057  rng2idl1cntr  21065  znfld  21336  ipassr2  21420  ocvin  21447  pjfo  21490  obsne0  21500  frlmgsum  21547  aspval2  21672  psrlinv  21736  mplsubglem  21778  mpllsslem  21779  evlslem4  21857  evlslem1  21865  mpfind  21890  evls1rhm  22062  madetsumid  22184  scmatcrng  22244  mdetleib2  22311  cramerimplem1  22406  m2pmfzgsumcl  22471  decpmatmul  22495  pmatcollpwscmat  22514  idpm2idmp  22524  pm2mpmhmlem1  22541  chpscmatgsummon  22568  chfacfscmulgsum  22583  chfacfpmmulgsum  22587  topbas  22696  uncld  22766  incld  22768  elcls  22798  neiptopnei  22857  resttopon  22886  restdis  22903  cnclima  22993  paste  23019  cncmp  23117  clsconn  23155  conncompcld  23159  1stcfb  23170  2ndcsb  23174  2ndcredom  23175  kgencmp2  23271  txss12  23330  qtoptop2  23424  qtoptopon  23429  hmphindis  23522  uffixfr  23648  ufildr  23656  isfcls2  23738  tgplacthmeo  23828  tsmsgsum  23864  tgptsmscld  23876  tsmssplit  23877  ustuqtop5  23971  uspreg  24000  prdsxmetlem  24095  prdsbl  24221  metss  24238  metrest  24254  nrmmetd  24304  isngp2  24327  ngpsubcan  24344  lssnlm  24439  nmoid  24480  opnreen  24568  mpomulcn  24606  evth  24706  htpyco2  24726  phtpyco2  24737  clmvz  24859  tcphcph  24986  iscmet3  25042  metcld  25055  bcthlem2  25074  cssbn  25124  chlcsschl  25127  minveclem1  25173  evthicc2  25210  ovolunlem1a  25246  ovolicc2lem1  25267  ovolicc2lem4  25270  ovolicc2lem5  25271  uniioombllem2  25333  uniioombllem3  25335  vitalilem2  25359  vitalilem4  25361  vitalilem5  25362  itg2monolem1  25501  cpnres  25688  rolle  25743  dvlip2  25748  dvivthlem2  25762  dvfsumrlimge0  25783  deg1pwle  25873  plydivlem4  26046  ulm0  26140  efif1olem1  26288  efif1olem2  26289  eflogeq  26347  argimlt0  26358  logrec  26505  relogbcxp  26527  atanlogadd  26656  atanlogsub  26658  atantan  26665  ftalem4  26817  ftalem5  26818  basellem3  26824  chtub  26952  dchrpt  27007  dchrsum2  27008  gausslemma2dlem1a  27105  2lgslem3a1  27140  2lgslem3b1  27141  2lgslem3c1  27142  2lgslem3d1  27143  2lgsoddprm  27156  dchrisumlem2  27230  pntrsumbnd2  27307  nosupbnd1lem4  27451  noinfbnd2lem1  27470  scutbdaylt  27557  oldlim  27619  madebday  27632  cofcutr  27650  negsbdaylem  27770  cnvmot  28060  tglineneq  28163  midexlem  28211  midex  28256  axlowdimlem14  28481  uhgrspansubgrlem  28815  usgrres  28833  usgrnbcnvfv  28890  finsumvtxdg2sstep  29074  uspgr2wlkeq  29171  redwlk  29197  pthdivtx  29254  usgr2wlkspthlem2  29283  wwlknvtx  29367  2wlkdlem6  29453  umgr2wlkon  29472  rusgrnumwwlk  29497  clwwlkwwlksb  29575  clwwlknwwlksnb  29576  clwwnisshclwwsn  29580  clwwlknscsh  29583  clwlknf1oclwwlknlem1  29602  1wlkdlem2  29659  fusgreghash2wsp  29859  2clwwlklem  29864  2clwwlk2clwwlk  29871  numclwwlk6  29911  ofrn2  32133  ofpreima2  32159  wrdsplex  32372  ccatf1  32383  mgcf1o  32441  gsumhashmul  32479  cycpmco2lem5  32560  cycpmco2lem6  32561  cycpmco2lem7  32562  cycpmco2  32563  cyc3co2  32570  imaslmod  32739  rspsnel  32759  elrspunidl  32821  qsidomlem1  32846  qsidomlem2  32847  dimpropd  32982  lbsdiflsp0  33000  extdg1id  33031  zarcmplem  33160  eulerpartlemgvv  33674  pfxwlk  34413  revwlk  34414  pthhashvtx  34417  spthcycl  34419  umgracycusgr  34444  subfacp1lem5  34474  satfvsucsuc  34655  cnambfre  36840  frlmvscadiccat  41387  ricdrng1  41407  pwsgprod  41417  evlsval3  41434  evlsbagval  41441  0prjspn  41673  3cubes  41731  oninfint  42288  onexomgt  42293  onexoegt  42296  ordeldif  42311  oacl2g  42383  onmcl  42384  omabs2  42385  omcl2  42386  tfsconcatfv  42394  tfsconcatrev  42401  ofoafg  42407  ofoafo  42409  ofoaass  42413  ofoacom  42414  onsucunifi  42423  oaun3lem1  42427  oadif1lem  42432  oadif1  42433  naddwordnexlem4  42455  safesnsupfilb  42472  gneispace  43188  rr-phpd  43265  grumnudlem  43347  ax6e2ndeqALT  43995  sineq0ALT  44001  fnresdmss  44166  saliinclf  45341  setsv  46345  sprsymrelfolem2  46460  lighneal  46578  isomuspgrlem2c  46797  lincresunit3  47250  2itscp  47555