Theorem syl2an2r 698

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5103  brcogw  5853  funfni  6670  f1un  6870  fvelimab  6983  dff3  7127  fnex  7249  ralima  7269  f1cofveqaeq  7287  f1eqcocnv  7335  caofid0l  7753  caofid0r  7754  caofid1  7755  caofid2  7756  onmindif2  7848  limsssuc  7888  mptcnfimad  8025  fnse  8180  frrlem13  8347  iinon  8379  smoord  8404  smoword  8405  tfrlem11  8427  coflton  8711  cofonr  8714  naddasslem2  8736  boxcutc  9000  f1domg  9029  phpeqd  9258  ominf  9286  f1finf1o  9295  unfilem1  9328  f1opwfi  9376  marypha2  9461  supmax  9490  infmin  9518  ordtypelem6  9547  oiexg  9559  oien  9562  cantnff  9705  cantnfp1lem3  9711  cantnflem1b  9717  cantnflem1  9720  ttrcltr  9747  ttrclselem2  9757  opwf  9850  rankopb  9896  xpnum  10062  infxpenlem  10122  infxp  10322  cflim2  10371  cofsmo  10377  cfsmolem  10378  cfcoflem  10380  ssfin3ds  10438  isf34lem5  10486  isf34lem6  10488  isfin1-3  10494  axcc3  10546  alephval2  10687  fpwwe2lem7  10752  canthp1  10769  tsken  10869  ltaddpr  11149  dedekind  11503  recextlem2  11977  recex  11978  gt0div  12213  ge0div  12214  lerec2  12235  uzwo2  13069  infssuzcl  13089  qmulcl  13125  xnegdi  13408  xmulpnf1n  13438  xadddi2  13457  fzm1  13771  2submod  14105  addmodlteq  14119  expnlbnd  14407  faclbnd5  14472  hasheni  14522  hashdifpr  14590  hashgt23el  14599  ccatrn  14765  ccatf1  14766  ccatalpha  14770  swrds1  14847  swrdccat2  14850  ccatpfx  14881  swrdccatin2  14909  pfxccatin12lem2  14911  revccat  14946  revrev  14947  swrdco  15019  relexpindlem  15248  resqrex  15449  fzomaxdiflem  15542  climconst  15742  serf0  15880  fsumf1o  15921  fsumrev  15977  fsumabs  16000  cvgcmp  16015  binomlem  16030  isumshft  16040  climcndslem1  16050  climcndslem2  16051  climcnds  16052  supcvg  16057  fprodcl2lem  16149  tanneg  16348  rpnnen2lem11  16424  modm1div  16466  fzo0dvdseq  16525  bitsfzolem  16636  gcdcllem3  16703  hashdvds  16984  prmdivdiv  16996  reumodprminv  17014  nnnn0modprm0  17016  pythagtrip  17044  dvdsprmpweqle  17096  pockthg  17116  4sqlem9  17156  vdwmc2  17189  vdwlem2  17192  imasaddflem  17734  acsfn1  17867  acsfn1c  17868  acsfn2  17869  oppccofval  17922  rescabs  18040  diag2  18451  grpinvalem  18886  issubmnd  18985  imasmnd  19001  pwsco2mhm  19061  gsumwspan  19074  frmdss2  19091  grpinvssd  19259  pwssub  19296  imasgrp  19298  subginv  19375  subginvcl  19377  ecqusaddcl  19440  ghmpreima  19484  conjnsg  19500  gass  19548  gsmsymgreqlem2  19678  f1omvdmvd  19690  symgsssg  19714  symgfisg  19715  symgtrinv  19719  psgnunilem5  19741  sylow1lem2  19846  odcau  19851  sylow2a  19866  sylow2  19873  efgsp1  19984  frgpuptf  20017  frgpuptinv  20018  frgpupf  20020  frgpup3lem  20024  mulgdi  20073  gsumval3eu  20151  gsumzsplit  20174  gsumzmhm  20184  gsumxp2  20227  prdsgsum  20228  fsfnn0gsumfsffz  20230  ablfaclem3  20336  srgbinomlem  20489  gsummgp0  20580  pwsgprod  20592  imasring  20593  dvdsr01  20634  rngisom1  20729  01eq0ring  20814  issubrng2  20843  subrgcrng  20860  subrginv  20873  isdrngd  21055  imadrhmcl  21087  abv1z  21114  lcomfsupp  21210  lmodvneg1  21213  lspsn  21310  lmhmco  21351  lmhmima  21355  lmhmpreima  21356  reslmhm  21360  lbsextlem2  21470  isridlrng  21531  lidl0cl  21532  lidlunin0  21548  rspvalint  21556  elrspsn  21558  rnglidlmmgm  21566  rnglidlmsgrp  21567  2idlcpblrng  21598  quscrng  21612  rngqiprngghmlem1  21616  rngqiprngghmlem3  21618  rngqiprnglinlem3  21622  rngqiprngimf1lem  21623  rngqiprngimf  21626  rng2idl1cntr  21634  qsidomlem1  21669  qsidomlem2  21670  ssdifidllem  21673  ssdifidlprm  21675  znfld  21899  ipassr2  21986  ocvin  22013  pjfo  22054  obsne0  22064  frlmgsum  22111  aspval2  22239  psrlinv  22296  mplsubglem  22339  mpllsslem  22340  evlslem4  22418  evlslem1  22424  evlsval3  22431  mpfind  22457  evls1rhm  22673  madetsumid  22809  scmatcrng  22869  mdetleib2  22936  cramerimplem1  23034  m2pmfzgsumcl  23099  decpmatmul  23123  pmatcollpwscmat  23142  idpm2idmp  23152  pm2mpmhmlem1  23169  chpscmatgsummon  23196  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  topbas  23323  uncld  23392  incld  23394  elcls  23424  neiptopnei  23483  resttopon  23512  restdis  23529  cnclima  23619  paste  23645  cncmp  23743  clsconn  23781  conncompcld  23785  1stcfb  23796  2ndcsb  23800  2ndcredom  23801  kgencmp2  23898  txss12  23957  qtoptop2  24051  qtoptopon  24056  hmphindis  24149  uffixfr  24275  ufildr  24283  isfcls2  24365  tgplacthmeo  24455  tsmsgsum  24491  tgptsmscld  24503  tsmssplit  24504  ustuqtop5  24597  uspreg  24625  prdsxmetlem  24720  prdsbl  24843  metss  24860  metrest  24876  nrmmetd  24926  isngp2  24949  ngpsubcan  24966  lssnlm  25053  nmoid  25094  opnreen  25184  mpomulcn  25221  evth  25313  htpyco2  25333  phtpyco2  25344  clmvz  25465  tcphcph  25591  iscmet3  25647  metcld  25660  bcthlem2  25679  cssbn  25729  chlcsschl  25732  minveclem1  25778  evthicc2  25814  ovolunlem1a  25850  ovolicc2lem1  25871  ovolicc2lem4  25874  ovolicc2lem5  25875  uniioombllem2  25937  uniioombllem3  25939  vitalilem2  25963  vitalilem4  25965  vitalilem5  25966  itg2monolem1  26104  cpnres  26290  rolle  26343  dvlip2  26348  dvivthlem2  26362  dvfsumrlimge0  26383  deg1pwle  26471  plydivlem4  26650  ulm0  26751  efif1olem1  26903  efif1olem2  26904  eflogeq  26963  argimlt0  26974  logrec  27124  relogbcxp  27146  atanlogadd  27275  atanlogsub  27277  atantan  27284  ftalem4  27436  ftalem5  27437  basellem3  27443  chtub  27572  dchrpt  27627  dchrsum2  27628  gausslemma2dlem1a  27725  2lgslem3a1  27760  2lgslem3b1  27761  2lgslem3c1  27762  2lgslem3d1  27763  2lgsoddprm  27776  dchrisumlem2  27850  pntrsumbnd2  27927  nosupbnd1lem4  28101  noinfbnd2lem1  28120  cutbdaylt  28217  oldlim  28306  madebday  28319  cofcutr  28343  addbday  28437  negbdaylem  28475  absmuls  28663  absnegs  28666  bdayfinlem  28905  cnvmot  29037  tglineneq  29146  midexlem  29197  midex  29246  plngrotlem1  29298  axlowdimlem14  29566  uhgrspansubgrlem  29904  usgrres  29922  usgrnbcnvfv  29979  finsumvtxdg2sstep  30163  uspgr2wlkeq  30259  redwlk  30284  pfxwlk  30299  revwlk  30300  pthdivtx  30345  pthhashvtx  30348  usgr2wlkspthlem2  30377  spthcycl  30425  wwlknvtx  30467  2wlkdlem6  30553  umgr2wlkon  30572  rusgrnumwwlk  30600  clwwlkwwlksb  30678  clwwlknwwlksnb  30679  clwwnisshclwwsn  30683  clwwlknscsh  30686  clwlknf1oclwwlknlem1  30705  1wlkdlem2  30762  fusgreghash2wsp  30972  2clwwlklem  30977  2clwwlk2clwwlk  30984  numclwwlk6  31024  prssad  33200  prssbd  33201  ofrn2  33309  ofpreima2  33335  sgnval2  33400  argcj  33413  wrdsplex  33576  mgcf1o  33640  gsumfs2d  33698  gsumhashmul  33704  gsummulsubdishift1  33705  cycpmco2lem5  33767  cycpmco2lem6  33768  cycpmco2lem7  33769  cycpmco2  33770  cyc3co2  33777  elrgspnlem1  33879  elrgspnlem2  33880  elrgspnsubrunlem1  33884  erler  33902  fracerl  33952  imaslmod  33998  elrspunidl  34062  ressply1evls1  34180  ply1coedeg  34204  esplyfval3  34287  exsslsb  34312  dimpropd  34324  lbsdiflsp0  34341  extdg1id  34381  madjusmdetlem2  34543  zarcmplem  34596  eulerpartlemgvv  35091  boolesineq  35170  fineqvnttrclselem1  35902  jltalephlem  36038  vonf1wev  36049  vonf1owevOLD  36051  umgracycusgr  36089  subfacp1lem5  36129  ptpconn  36178  satfvsucsuc  36310  ply1divalg3  36587  weiunfrlem  37443  ttctr  37472  dfttc2g  37485  cnambfre  38791  mapdordlem2  42897  frlmvscadiccat  43777  ricdrng1  43796  evlsbagval  43818  0prjspn  43868  3cubes  43904  oninfint  44441  onexomgt  44446  onexoegt  44449  ordeldif  44463  oacl2g  44535  onmcl  44536  omabs2  44537  omcl2  44538  tfsconcatfv  44546  tfsconcatrev  44553  ofoafg  44559  ofoafo  44561  ofoaass  44565  ofoacom  44566  onsucunifi  44575  oaun3lem1  44579  oadif1lem  44584  oadif1  44585  naddwordnexlem4  44606  safesnsupfilb  44622  gneispace  45337  rr-phpd  45410  grumnudlem  45472  ax6e2ndeqALT  46115  sineq0ALT  46121  hashnnlt  46218  fnresdmss  46398  saliinclf  47551  hoicvr  47773  tmachlem-agreeprod  48162  setsv  48675  sprsymrelfolem2  48790  lighneal  48911  indprmfz  48930  grimuhgr  49200  grimcnv  49201  uhgrimedgi  49203  uhgrimedg  49204  isuspgrim0lem  49206  isuspgrim0  49207  upgrimtrlslem1  49217  upgrimtrlslem2  49218  clnbgrgrim  49247  grimedg  49248  isubgr3stgrlem8  49286  clnbgr3stgrgrlim  49332  clnbgr3stgrgrlic  49333  lincresunit3  49808  2itscp  50108  resccat  50403  tanhneg  51136