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  5100  brcogw  5846  funfni  6637  f1un  6837  fvelimab  6949  dff3  7092  fnex  7215  ralima  7235  f1cofveqaeq  7253  f1eqcocnv  7301  caofid0l  7715  caofid0r  7716  caofid1  7717  caofid2  7718  onmindif2  7810  limsssuc  7850  mptcnfimad  7987  fnse  8134  frrlem13  8300  iinon  8332  smoord  8357  smoword  8358  tfrlem11  8380  coflton  8664  cofonr  8667  naddasslem2  8689  boxcutc  8953  f1domg  8982  phpeqd  9211  ominf  9239  f1finf1o  9248  unfilem1  9281  f1opwfi  9329  marypha2  9415  supmax  9444  infmin  9472  ordtypelem6  9501  oiexg  9513  oien  9516  cantnff  9659  cantnfp1lem3  9665  cantnflem1b  9671  cantnflem1  9674  ttrcltr  9701  ttrclselem2  9711  opwf  9802  rankopb  9847  xpnum  10013  infxpenlem  10073  infxp  10273  cflim2  10322  cofsmo  10328  cfsmolem  10329  cfcoflem  10331  ssfin3ds  10389  isf34lem5  10437  isf34lem6  10439  isfin1-3  10445  axcc3  10497  alephval2  10638  fpwwe2lem7  10703  canthp1  10720  tsken  10820  ltaddpr  11100  dedekind  11454  recextlem2  11928  recex  11929  gt0div  12164  ge0div  12165  lerec2  12186  uzwo2  13020  infssuzcl  13040  qmulcl  13076  xnegdi  13359  xmulpnf1n  13389  xadddi2  13408  fzm1  13721  2submod  14055  addmodlteq  14069  expnlbnd  14357  faclbnd5  14422  hasheni  14472  hashdifpr  14540  hashgt23el  14549  ccatrn  14715  ccatf1  14716  ccatalpha  14720  swrds1  14796  swrdccat2  14799  ccatpfx  14830  swrdccatin2  14858  pfxccatin12lem2  14860  revccat  14895  revrev  14896  swrdco  14968  relexpindlem  15196  resqrex  15397  fzomaxdiflem  15490  climconst  15690  serf0  15828  fsumf1o  15869  fsumrev  15925  fsumabs  15948  cvgcmp  15963  binomlem  15978  isumshft  15988  climcndslem1  15998  climcndslem2  15999  climcnds  16000  supcvg  16005  fprodcl2lem  16097  tanneg  16296  rpnnen2lem11  16372  modm1div  16414  fzo0dvdseq  16473  bitsfzolem  16584  gcdcllem3  16651  hashdvds  16932  prmdivdiv  16944  reumodprminv  16962  nnnn0modprm0  16964  pythagtrip  16992  dvdsprmpweqle  17044  pockthg  17064  4sqlem9  17104  vdwmc2  17137  vdwlem2  17140  imasaddflem  17682  acsfn1  17815  acsfn1c  17816  acsfn2  17817  oppccofval  17870  rescabs  17988  diag2  18399  grpinvalem  18834  issubmnd  18933  imasmnd  18949  pwsco2mhm  19009  gsumwspan  19022  frmdss2  19039  grpinvssd  19207  pwssub  19244  imasgrp  19246  subginv  19323  subginvcl  19325  ecqusaddcl  19388  ghmpreima  19432  conjnsg  19448  gass  19495  gsmsymgreqlem2  19625  f1omvdmvd  19637  symgsssg  19661  symgfisg  19662  symgtrinv  19666  psgnunilem5  19688  sylow1lem2  19793  odcau  19798  sylow2a  19813  sylow2  19820  efgsp1  19931  frgpuptf  19964  frgpuptinv  19965  frgpupf  19967  frgpup3lem  19971  mulgdi  20020  gsumval3eu  20098  gsumzsplit  20121  gsumzmhm  20131  gsumxp2  20174  prdsgsum  20175  fsfnn0gsumfsffz  20177  ablfaclem3  20283  srgbinomlem  20436  gsummgp0  20527  pwsgprod  20539  imasring  20540  dvdsr01  20581  rngisom1  20676  01eq0ring  20761  issubrng2  20790  subrgcrng  20807  subrginv  20820  isdrngd  21002  imadrhmcl  21034  abv1z  21061  lcomfsupp  21157  lmodvneg1  21160  lspsn  21257  lmhmco  21298  lmhmima  21302  lmhmpreima  21303  reslmhm  21307  lbsextlem2  21417  isridlrng  21478  lidl0cl  21479  lidlunin0  21495  rspvalint  21503  elrspsn  21505  rnglidlmmgm  21513  rnglidlmsgrp  21514  2idlcpblrng  21545  quscrng  21559  rngqiprngghmlem1  21563  rngqiprngghmlem3  21565  rngqiprnglinlem3  21569  rngqiprngimf1lem  21570  rngqiprngimf  21573  rng2idl1cntr  21581  qsidomlem1  21616  qsidomlem2  21617  ssdifidllem  21620  ssdifidlprm  21622  znfld  21846  ipassr2  21933  ocvin  21960  pjfo  22001  obsne0  22011  frlmgsum  22058  aspval2  22186  psrlinv  22243  mplsubglem  22286  mpllsslem  22287  evlslem4  22365  evlslem1  22371  evlsval3  22378  mpfind  22404  evls1rhm  22620  madetsumid  22756  scmatcrng  22816  mdetleib2  22883  cramerimplem1  22981  m2pmfzgsumcl  23046  decpmatmul  23070  pmatcollpwscmat  23089  idpm2idmp  23099  pm2mpmhmlem1  23116  chpscmatgsummon  23143  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  topbas  23270  uncld  23339  incld  23341  elcls  23371  neiptopnei  23430  resttopon  23459  restdis  23476  cnclima  23566  paste  23592  cncmp  23690  clsconn  23728  conncompcld  23732  1stcfb  23743  2ndcsb  23747  2ndcredom  23748  kgencmp2  23845  txss12  23904  qtoptop2  23998  qtoptopon  24003  hmphindis  24096  uffixfr  24222  ufildr  24230  isfcls2  24312  tgplacthmeo  24402  tsmsgsum  24438  tgptsmscld  24450  tsmssplit  24451  ustuqtop5  24544  uspreg  24572  prdsxmetlem  24667  prdsbl  24790  metss  24807  metrest  24823  nrmmetd  24873  isngp2  24896  ngpsubcan  24913  lssnlm  25000  nmoid  25041  opnreen  25131  mpomulcn  25168  evth  25260  htpyco2  25280  phtpyco2  25291  clmvz  25412  tcphcph  25538  iscmet3  25594  metcld  25607  bcthlem2  25626  cssbn  25676  chlcsschl  25679  minveclem1  25725  evthicc2  25761  ovolunlem1a  25797  ovolicc2lem1  25818  ovolicc2lem4  25821  ovolicc2lem5  25822  uniioombllem2  25884  uniioombllem3  25886  vitalilem2  25910  vitalilem4  25912  vitalilem5  25913  itg2monolem1  26051  cpnres  26237  rolle  26290  dvlip2  26295  dvivthlem2  26309  dvfsumrlimge0  26330  deg1pwle  26418  plydivlem4  26599  ulm0  26700  efif1olem1  26852  efif1olem2  26853  eflogeq  26912  argimlt0  26923  logrec  27073  relogbcxp  27095  atanlogadd  27224  atanlogsub  27226  atantan  27233  ftalem4  27385  ftalem5  27386  basellem3  27392  chtub  27521  dchrpt  27576  dchrsum2  27577  gausslemma2dlem1a  27674  2lgslem3a1  27709  2lgslem3b1  27710  2lgslem3c1  27711  2lgslem3d1  27712  2lgsoddprm  27725  dchrisumlem2  27799  pntrsumbnd2  27876  nosupbnd1lem4  28050  noinfbnd2lem1  28069  cutbdaylt  28166  oldlim  28255  madebday  28268  cofcutr  28292  addbday  28386  negbdaylem  28424  absmuls  28612  absnegs  28615  bdayfinlem  28854  cnvmot  28986  tglineneq  29095  midexlem  29146  midex  29195  plngrotlem1  29247  axlowdimlem14  29515  uhgrspansubgrlem  29853  usgrres  29871  usgrnbcnvfv  29928  finsumvtxdg2sstep  30112  uspgr2wlkeq  30208  redwlk  30233  pfxwlk  30248  revwlk  30249  pthdivtx  30294  pthhashvtx  30297  usgr2wlkspthlem2  30326  spthcycl  30374  wwlknvtx  30416  2wlkdlem6  30502  umgr2wlkon  30521  rusgrnumwwlk  30549  clwwlkwwlksb  30627  clwwlknwwlksnb  30628  clwwnisshclwwsn  30632  clwwlknscsh  30635  clwlknf1oclwwlknlem1  30654  1wlkdlem2  30711  fusgreghash2wsp  30921  2clwwlklem  30926  2clwwlk2clwwlk  30933  numclwwlk6  30973  prssad  33107  prssbd  33108  ofrn2  33216  ofpreima2  33242  sgnval2  33309  argcj  33322  wrdsplex  33485  mgcf1o  33546  gsumfs2d  33604  gsumhashmul  33610  gsummulsubdishift1  33611  cycpmco2lem5  33673  cycpmco2lem6  33674  cycpmco2lem7  33675  cycpmco2  33676  cyc3co2  33683  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnsubrunlem1  33790  erler  33808  fracerl  33850  imaslmod  33896  elrspunidl  33960  ressply1evls1  34079  ply1coedeg  34103  esplyfval3  34186  exsslsb  34211  dimpropd  34223  lbsdiflsp0  34240  extdg1id  34280  madjusmdetlem2  34442  zarcmplem  34495  eulerpartlemgvv  34991  boolesineq  35070  fineqvnttrclselem1  35762  vonf1wev  35860  vonf1owevOLD  35862  umgracycusgr  35888  subfacp1lem5  35918  satfvsucsuc  36099  ply1divalg3  36376  weiunfrlem  37222  ttctr  37251  dfttc2g  37264  cnambfre  38554  mapdordlem2  42662  frlmvscadiccat  43538  ricdrng1  43554  evlsbagval  43576  0prjspn  43618  3cubes  43654  oninfint  44196  onexomgt  44201  onexoegt  44204  ordeldif  44218  oacl2g  44290  onmcl  44291  omabs2  44292  omcl2  44293  tfsconcatfv  44301  tfsconcatrev  44308  ofoafg  44314  ofoafo  44316  ofoaass  44320  ofoacom  44321  onsucunifi  44330  oaun3lem1  44334  oadif1lem  44339  oadif1  44340  naddwordnexlem4  44361  safesnsupfilb  44377  gneispace  45093  rr-phpd  45166  grumnudlem  45228  ax6e2ndeqALT  45872  sineq0ALT  45878  hashnnlt  45964  fnresdmss  46126  saliinclf  47280  hoicvr  47502  tmachlem-agreeprod  47891  setsv  48404  sprsymrelfolem2  48519  lighneal  48640  indprmfz  48659  grimuhgr  48929  grimcnv  48930  uhgrimedgi  48932  uhgrimedg  48933  isuspgrim0lem  48935  isuspgrim0  48936  upgrimtrlslem1  48946  upgrimtrlslem2  48947  clnbgrgrim  48976  grimedg  48977  isubgr3stgrlem8  49015  clnbgr3stgrgrlim  49061  clnbgr3stgrgrlic  49062  lincresunit3  49537  2itscp  49837  resccat  50126