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  5099  brcogw  5845  funfni  6645  f1un  6845  fvelimab  6957  dff3  7100  fnex  7223  ralima  7243  f1cofveqaeq  7261  f1eqcocnv  7309  caofid0l  7726  caofid0r  7727  caofid1  7728  caofid2  7729  onmindif2  7821  limsssuc  7861  mptcnfimad  7998  fnse  8152  frrlem13  8319  iinon  8351  smoord  8376  smoword  8377  tfrlem11  8399  coflton  8683  cofonr  8686  naddasslem2  8708  boxcutc  8972  f1domg  9001  phpeqd  9230  ominf  9258  f1finf1o  9267  unfilem1  9300  f1opwfi  9348  marypha2  9434  supmax  9463  infmin  9491  ordtypelem6  9520  oiexg  9532  oien  9535  cantnff  9678  cantnfp1lem3  9684  cantnflem1b  9690  cantnflem1  9693  ttrcltr  9720  ttrclselem2  9730  opwf  9823  rankopb  9869  xpnum  10035  infxpenlem  10095  infxp  10295  cflim2  10344  cofsmo  10350  cfsmolem  10351  cfcoflem  10353  ssfin3ds  10411  isf34lem5  10459  isf34lem6  10461  isfin1-3  10467  axcc3  10519  alephval2  10660  fpwwe2lem7  10725  canthp1  10742  tsken  10842  ltaddpr  11122  dedekind  11476  recextlem2  11950  recex  11951  gt0div  12186  ge0div  12187  lerec2  12208  uzwo2  13042  infssuzcl  13062  qmulcl  13098  xnegdi  13381  xmulpnf1n  13411  xadddi2  13430  fzm1  13744  2submod  14078  addmodlteq  14092  expnlbnd  14380  faclbnd5  14445  hasheni  14495  hashdifpr  14563  hashgt23el  14572  ccatrn  14738  ccatf1  14739  ccatalpha  14743  swrds1  14820  swrdccat2  14823  ccatpfx  14854  swrdccatin2  14882  pfxccatin12lem2  14884  revccat  14919  revrev  14920  swrdco  14992  relexpindlem  15221  resqrex  15422  fzomaxdiflem  15515  climconst  15715  serf0  15853  fsumf1o  15894  fsumrev  15950  fsumabs  15973  cvgcmp  15988  binomlem  16003  isumshft  16013  climcndslem1  16023  climcndslem2  16024  climcnds  16025  supcvg  16030  fprodcl2lem  16122  tanneg  16321  rpnnen2lem11  16397  modm1div  16439  fzo0dvdseq  16498  bitsfzolem  16609  gcdcllem3  16676  hashdvds  16957  prmdivdiv  16969  reumodprminv  16987  nnnn0modprm0  16989  pythagtrip  17017  dvdsprmpweqle  17069  pockthg  17089  4sqlem9  17129  vdwmc2  17162  vdwlem2  17165  imasaddflem  17707  acsfn1  17840  acsfn1c  17841  acsfn2  17842  oppccofval  17895  rescabs  18013  diag2  18424  grpinvalem  18859  issubmnd  18958  imasmnd  18974  pwsco2mhm  19034  gsumwspan  19047  frmdss2  19064  grpinvssd  19232  pwssub  19269  imasgrp  19271  subginv  19348  subginvcl  19350  ecqusaddcl  19413  ghmpreima  19457  conjnsg  19473  gass  19520  gsmsymgreqlem2  19650  f1omvdmvd  19662  symgsssg  19686  symgfisg  19687  symgtrinv  19691  psgnunilem5  19713  sylow1lem2  19818  odcau  19823  sylow2a  19838  sylow2  19845  efgsp1  19956  frgpuptf  19989  frgpuptinv  19990  frgpupf  19992  frgpup3lem  19996  mulgdi  20045  gsumval3eu  20123  gsumzsplit  20146  gsumzmhm  20156  gsumxp2  20199  prdsgsum  20200  fsfnn0gsumfsffz  20202  ablfaclem3  20308  srgbinomlem  20461  gsummgp0  20552  pwsgprod  20564  imasring  20565  dvdsr01  20606  rngisom1  20701  01eq0ring  20786  issubrng2  20815  subrgcrng  20832  subrginv  20845  isdrngd  21027  imadrhmcl  21059  abv1z  21086  lcomfsupp  21182  lmodvneg1  21185  lspsn  21282  lmhmco  21323  lmhmima  21327  lmhmpreima  21328  reslmhm  21332  lbsextlem2  21442  isridlrng  21503  lidl0cl  21504  lidlunin0  21520  rspvalint  21528  elrspsn  21530  rnglidlmmgm  21538  rnglidlmsgrp  21539  2idlcpblrng  21570  quscrng  21584  rngqiprngghmlem1  21588  rngqiprngghmlem3  21590  rngqiprnglinlem3  21594  rngqiprngimf1lem  21595  rngqiprngimf  21598  rng2idl1cntr  21606  qsidomlem1  21641  qsidomlem2  21642  ssdifidllem  21645  ssdifidlprm  21647  znfld  21871  ipassr2  21958  ocvin  21985  pjfo  22026  obsne0  22036  frlmgsum  22083  aspval2  22211  psrlinv  22268  mplsubglem  22311  mpllsslem  22312  evlslem4  22390  evlslem1  22396  evlsval3  22403  mpfind  22429  evls1rhm  22645  madetsumid  22781  scmatcrng  22841  mdetleib2  22908  cramerimplem1  23006  m2pmfzgsumcl  23071  decpmatmul  23095  pmatcollpwscmat  23114  idpm2idmp  23124  pm2mpmhmlem1  23141  chpscmatgsummon  23168  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  topbas  23295  uncld  23364  incld  23366  elcls  23396  neiptopnei  23455  resttopon  23484  restdis  23501  cnclima  23591  paste  23617  cncmp  23715  clsconn  23753  conncompcld  23757  1stcfb  23768  2ndcsb  23772  2ndcredom  23773  kgencmp2  23870  txss12  23929  qtoptop2  24023  qtoptopon  24028  hmphindis  24121  uffixfr  24247  ufildr  24255  isfcls2  24337  tgplacthmeo  24427  tsmsgsum  24463  tgptsmscld  24475  tsmssplit  24476  ustuqtop5  24569  uspreg  24597  prdsxmetlem  24692  prdsbl  24815  metss  24832  metrest  24848  nrmmetd  24898  isngp2  24921  ngpsubcan  24938  lssnlm  25025  nmoid  25066  opnreen  25156  mpomulcn  25193  evth  25285  htpyco2  25305  phtpyco2  25316  clmvz  25437  tcphcph  25563  iscmet3  25619  metcld  25632  bcthlem2  25651  cssbn  25701  chlcsschl  25704  minveclem1  25750  evthicc2  25786  ovolunlem1a  25822  ovolicc2lem1  25843  ovolicc2lem4  25846  ovolicc2lem5  25847  uniioombllem2  25909  uniioombllem3  25911  vitalilem2  25935  vitalilem4  25937  vitalilem5  25938  itg2monolem1  26076  cpnres  26262  rolle  26315  dvlip2  26320  dvivthlem2  26334  dvfsumrlimge0  26355  deg1pwle  26443  plydivlem4  26622  ulm0  26723  efif1olem1  26875  efif1olem2  26876  eflogeq  26935  argimlt0  26946  logrec  27096  relogbcxp  27118  atanlogadd  27247  atanlogsub  27249  atantan  27256  ftalem4  27408  ftalem5  27409  basellem3  27415  chtub  27544  dchrpt  27599  dchrsum2  27600  gausslemma2dlem1a  27697  2lgslem3a1  27732  2lgslem3b1  27733  2lgslem3c1  27734  2lgslem3d1  27735  2lgsoddprm  27748  dchrisumlem2  27822  pntrsumbnd2  27899  nosupbnd1lem4  28073  noinfbnd2lem1  28092  cutbdaylt  28189  oldlim  28278  madebday  28291  cofcutr  28315  addbday  28409  negbdaylem  28447  absmuls  28635  absnegs  28638  bdayfinlem  28877  cnvmot  29009  tglineneq  29118  midexlem  29169  midex  29218  plngrotlem1  29270  axlowdimlem14  29538  uhgrspansubgrlem  29876  usgrres  29894  usgrnbcnvfv  29951  finsumvtxdg2sstep  30135  uspgr2wlkeq  30231  redwlk  30256  pfxwlk  30271  revwlk  30272  pthdivtx  30317  pthhashvtx  30320  usgr2wlkspthlem2  30349  spthcycl  30397  wwlknvtx  30439  2wlkdlem6  30525  umgr2wlkon  30544  rusgrnumwwlk  30572  clwwlkwwlksb  30650  clwwlknwwlksnb  30651  clwwnisshclwwsn  30655  clwwlknscsh  30658  clwlknf1oclwwlknlem1  30677  1wlkdlem2  30734  fusgreghash2wsp  30944  2clwwlklem  30949  2clwwlk2clwwlk  30956  numclwwlk6  30996  prssad  33172  prssbd  33173  ofrn2  33281  ofpreima2  33307  sgnval2  33373  argcj  33386  wrdsplex  33549  mgcf1o  33610  gsumfs2d  33668  gsumhashmul  33674  gsummulsubdishift1  33675  cycpmco2lem5  33737  cycpmco2lem6  33738  cycpmco2lem7  33739  cycpmco2  33740  cyc3co2  33747  elrgspnlem1  33849  elrgspnlem2  33850  elrgspnsubrunlem1  33854  erler  33872  fracerl  33914  imaslmod  33960  elrspunidl  34024  ressply1evls1  34143  ply1coedeg  34167  esplyfval3  34250  exsslsb  34275  dimpropd  34287  lbsdiflsp0  34304  extdg1id  34344  madjusmdetlem2  34506  zarcmplem  34559  eulerpartlemgvv  35054  boolesineq  35133  fineqvnttrclselem1  35845  vonf1wev  35955  vonf1owevOLD  35957  umgracycusgr  35995  subfacp1lem5  36035  ptpconn  36084  satfvsucsuc  36216  ply1divalg3  36493  weiunfrlem  37344  ttctr  37373  dfttc2g  37386  cnambfre  38679  mapdordlem2  42787  frlmvscadiccat  43666  ricdrng1  43685  evlsbagval  43707  0prjspn  43757  3cubes  43793  oninfint  44331  onexomgt  44336  onexoegt  44339  ordeldif  44353  oacl2g  44425  onmcl  44426  omabs2  44427  omcl2  44428  tfsconcatfv  44436  tfsconcatrev  44443  ofoafg  44449  ofoafo  44451  ofoaass  44455  ofoacom  44456  onsucunifi  44465  oaun3lem1  44469  oadif1lem  44474  oadif1  44475  naddwordnexlem4  44496  safesnsupfilb  44512  gneispace  45227  rr-phpd  45300  grumnudlem  45362  ax6e2ndeqALT  46006  sineq0ALT  46012  hashnnlt  46105  fnresdmss  46276  saliinclf  47429  hoicvr  47651  tmachlem-agreeprod  48040  setsv  48553  sprsymrelfolem2  48668  lighneal  48789  indprmfz  48808  grimuhgr  49078  grimcnv  49079  uhgrimedgi  49081  uhgrimedg  49082  isuspgrim0lem  49084  isuspgrim0  49085  upgrimtrlslem1  49095  upgrimtrlslem2  49096  clnbgrgrim  49125  grimedg  49126  isubgr3stgrlem8  49164  clnbgr3stgrgrlim  49210  clnbgr3stgrgrlic  49211  lincresunit3  49686  2itscp  49986  resccat  50281