Theorem syl2an2r 691

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  disjxiun  5076  axprlem4OLD  5366  brcogw  5817  funfni  6598  f1un  6794  fvelimab  6906  dff3  7048  fnex  7168  ralima  7188  f1cofveqaeq  7208  f1eqcocnv  7252  caofid0l  7660  caofid0r  7661  caofid1  7662  caofid2  7663  onmindif2  7757  limsssuc  7797  mptcnfimad  7935  fnse  8080  frrlem13  8245  iinon  8277  smoord  8302  smoword  8303  tfrlem11  8324  coflton  8604  cofonr  8607  naddasslem2  8628  boxcutc  8886  f1domg  8915  phpeqd  9143  ominf  9171  f1finf1o  9180  unfilem1  9212  f1opwfi  9263  marypha2  9349  supmax  9378  infmin  9406  ordtypelem6  9435  oiexg  9447  oien  9450  cantnff  9593  cantnfp1lem3  9599  cantnflem1b  9605  cantnflem1  9608  ttrcltr  9635  ttrclselem2  9645  opwf  9734  rankopb  9774  xpnum  9873  infxpenlem  9933  infxp  10134  cflim2  10183  cofsmo  10189  cfsmolem  10190  cfcoflem  10192  ssfin3ds  10250  isf34lem5  10298  isf34lem6  10300  isfin1-3  10306  axcc3  10358  alephval2  10493  fpwwe2lem7  10558  canthp1  10575  tsken  10675  ltaddpr  10955  dedekind  11307  recextlem2  11779  recex  11780  gt0div  12020  ge0div  12021  lerec2  12042  uzwo2  12860  infssuzcl  12880  qmulcl  12915  xnegdi  13198  xmulpnf1n  13228  xadddi2  13247  fzm1  13559  2submod  13892  addmodlteq  13906  expnlbnd  14193  faclbnd5  14258  hasheni  14308  hashdifpr  14375  hashgt23el  14384  ccatrn  14550  ccatalpha  14554  swrds1  14627  swrdccat2  14630  ccatpfx  14661  swrdccatin2  14689  pfxccatin12lem2  14691  revccat  14726  revrev  14727  swrdco  14797  relexpindlem  15023  resqrex  15210  fzomaxdiflem  15303  climconst  15503  serf0  15641  fsumf1o  15683  fsumrev  15739  fsumabs  15762  cvgcmp  15777  binomlem  15792  isumshft  15802  climcndslem1  15812  climcndslem2  15813  climcnds  15814  supcvg  15819  fprodcl2lem  15913  tanneg  16113  rpnnen2lem11  16189  modm1div  16231  fzo0dvdseq  16290  bitsfzolem  16401  gcdcllem3  16468  hashdvds  16743  prmdivdiv  16755  reumodprminv  16773  nnnn0modprm0  16775  pythagtrip  16803  dvdsprmpweqle  16855  pockthg  16875  4sqlem9  16915  vdwmc2  16948  vdwlem2  16951  imasaddflem  17492  acsfn1  17625  acsfn1c  17626  acsfn2  17627  oppccofval  17680  rescabs  17798  diag2  18209  grpinvalem  18639  issubmnd  18727  imasmnd  18741  pwsco2mhm  18799  gsumwspan  18812  frmdss2  18829  grpinvssd  18991  pwssub  19028  imasgrp  19030  subginv  19107  subginvcl  19109  ecqusaddcl  19166  ghmpreima  19211  conjnsg  19227  gass  19274  gsmsymgreqlem2  19404  f1omvdmvd  19416  symgsssg  19440  symgfisg  19441  symgtrinv  19445  psgnunilem5  19467  sylow1lem2  19572  odcau  19577  sylow2a  19592  sylow2  19599  efgsp1  19710  frgpuptf  19743  frgpuptinv  19744  frgpupf  19746  frgpup3lem  19750  mulgdi  19799  gsumval3eu  19877  gsumzsplit  19900  gsumzmhm  19910  gsumxp2  19953  prdsgsum  19954  fsfnn0gsumfsffz  19956  ablfaclem3  20062  srgbinomlem  20209  gsummgp0  20295  pwsgprod  20307  imasring  20308  dvdsr01  20349  rngisom1  20444  01eq0ring  20509  issubrng2  20537  subrgcrng  20554  subrginv  20567  isdrngd  20744  imadrhmcl  20776  abv1z  20803  lcomfsupp  20899  lmodvneg1  20902  lspsn  20999  lmhmco  21040  lmhmima  21044  lmhmpreima  21045  reslmhm  21049  lbsextlem2  21159  isridlrng  21219  lidl0cl  21220  elrspsn  21240  rnglidlmmgm  21245  rnglidlmsgrp  21246  2idlcpblrng  21271  quscrng  21283  rngqiprngghmlem1  21287  rngqiprngghmlem3  21289  rngqiprnglinlem3  21293  rngqiprngimf1lem  21294  rngqiprngimf  21297  rng2idl1cntr  21305  znfld  21542  ipassr2  21629  ocvin  21656  pjfo  21697  obsne0  21707  frlmgsum  21754  aspval2  21880  psrlinv  21937  mplsubglem  21980  mpllsslem  21981  evlslem4  22059  evlslem1  22065  evlsval3  22072  mpfind  22098  evls1rhm  22315  madetsumid  22451  scmatcrng  22511  mdetleib2  22578  cramerimplem1  22673  m2pmfzgsumcl  22738  decpmatmul  22762  pmatcollpwscmat  22781  idpm2idmp  22791  pm2mpmhmlem1  22808  chpscmatgsummon  22835  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  topbas  22962  uncld  23031  incld  23033  elcls  23063  neiptopnei  23122  resttopon  23151  restdis  23168  cnclima  23258  paste  23284  cncmp  23382  clsconn  23420  conncompcld  23424  1stcfb  23435  2ndcsb  23439  2ndcredom  23440  kgencmp2  23536  txss12  23595  qtoptop2  23689  qtoptopon  23694  hmphindis  23787  uffixfr  23913  ufildr  23921  isfcls2  24003  tgplacthmeo  24093  tsmsgsum  24129  tgptsmscld  24141  tsmssplit  24142  ustuqtop5  24235  uspreg  24263  prdsxmetlem  24358  prdsbl  24481  metss  24498  metrest  24514  nrmmetd  24564  isngp2  24587  ngpsubcan  24604  lssnlm  24691  nmoid  24732  opnreen  24822  mpomulcn  24859  evth  24951  htpyco2  24971  phtpyco2  24982  clmvz  25103  tcphcph  25229  iscmet3  25285  metcld  25298  bcthlem2  25317  cssbn  25367  chlcsschl  25370  minveclem1  25416  evthicc2  25452  ovolunlem1a  25488  ovolicc2lem1  25509  ovolicc2lem4  25512  ovolicc2lem5  25513  uniioombllem2  25575  uniioombllem3  25577  vitalilem2  25601  vitalilem4  25603  vitalilem5  25604  itg2monolem1  25742  cpnres  25929  rolle  25982  dvlip2  25987  dvivthlem2  26001  dvfsumrlimge0  26022  deg1pwle  26110  plydivlem4  26287  ulm0  26381  efif1olem1  26531  efif1olem2  26532  eflogeq  26591  argimlt0  26602  logrec  26752  relogbcxp  26774  atanlogadd  26903  atanlogsub  26905  atantan  26912  ftalem4  27064  ftalem5  27065  basellem3  27071  chtub  27200  dchrpt  27255  dchrsum2  27256  gausslemma2dlem1a  27353  2lgslem3a1  27388  2lgslem3b1  27389  2lgslem3c1  27390  2lgslem3d1  27391  2lgsoddprm  27404  dchrisumlem2  27478  pntrsumbnd2  27555  nosupbnd1lem4  27700  noinfbnd2lem1  27719  cutbdaylt  27815  oldlim  27904  madebday  27917  cofcutr  27941  addbday  28035  negbdaylem  28073  absmuls  28261  absnegs  28264  bdayfinlem  28503  cnvmot  28634  tglineneq  28737  midexlem  28785  midex  28830  axlowdimlem14  29049  uhgrspansubgrlem  29384  usgrres  29402  usgrnbcnvfv  29459  finsumvtxdg2sstep  29643  uspgr2wlkeq  29739  redwlk  29764  pthdivtx  29820  usgr2wlkspthlem2  29851  wwlknvtx  29938  2wlkdlem6  30024  umgr2wlkon  30043  rusgrnumwwlk  30071  clwwlkwwlksb  30149  clwwlknwwlksnb  30150  clwwnisshclwwsn  30154  clwwlknscsh  30157  clwlknf1oclwwlknlem1  30176  1wlkdlem2  30233  fusgreghash2wsp  30433  2clwwlklem  30438  2clwwlk2clwwlk  30445  numclwwlk6  30485  prssad  32624  prssbd  32625  ofrn2  32739  ofpreima2  32765  sgnval2  32834  argcj  32847  wrdsplex  33022  ccatf1  33035  mgcf1o  33089  gsumfs2d  33149  gsumhashmul  33155  gsummulsubdishift1  33156  cycpmco2lem5  33218  cycpmco2lem6  33219  cycpmco2lem7  33220  cycpmco2  33221  cyc3co2  33228  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnsubrunlem1  33335  erler  33353  fracerl  33397  imaslmod  33443  elrspunidl  33518  qsidomlem1  33542  qsidomlem2  33543  ssdifidllem  33546  ssdifidlprm  33548  ressply1evls1  33655  ply1coedeg  33679  esplyfval3  33763  exsslsb  33788  dimpropd  33800  lbsdiflsp0  33817  extdg1id  33857  madjusmdetlem2  34019  zarcmplem  34072  eulerpartlemgvv  34567  boolesineq  34646  fineqvnttrclselem1  35309  vonf1owev  35343  pfxwlk  35359  revwlk  35360  pthhashvtx  35363  spthcycl  35364  umgracycusgr  35389  subfacp1lem5  35419  satfvsucsuc  35600  ply1divalg3  35877  weiunfrlem  36699  ttctr  36728  dfttc2g  36741  cnambfre  38042  mapdordlem2  42136  frlmvscadiccat  43003  ricdrng1  43021  evlsbagval  43043  0prjspn  43085  3cubes  43146  oninfint  43688  onexomgt  43693  onexoegt  43696  ordeldif  43710  oacl2g  43782  onmcl  43783  omabs2  43784  omcl2  43785  tfsconcatfv  43793  tfsconcatrev  43800  ofoafg  43806  ofoafo  43808  ofoaass  43812  ofoacom  43813  onsucunifi  43822  oaun3lem1  43826  oadif1lem  43831  oadif1  43832  naddwordnexlem4  43853  safesnsupfilb  43869  gneispace  44585  rr-phpd  44660  grumnudlem  44736  ax6e2ndeqALT  45381  sineq0ALT  45387  fnresdmss  45622  saliinclf  46776  hoicvr  46998  setsv  47860  sprsymrelfolem2  47975  lighneal  48096  indprmfz  48115  grimuhgr  48385  grimcnv  48386  uhgrimedgi  48388  uhgrimedg  48389  isuspgrim0lem  48391  isuspgrim0  48392  upgrimtrlslem1  48402  upgrimtrlslem2  48403  clnbgrgrim  48432  grimedg  48433  isubgr3stgrlem8  48471  clnbgr3stgrgrlim  48517  clnbgr3stgrgrlic  48518  lincresunit3  48979  2itscp  49279  resccat  49571