Theorem syl2an2r 686

Description: syl2anr 598 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 581	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 592	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 207  df-an 396

This theorem is referenced by:  disjxiun  5082  axprlem4OLD  5372  brcogw  5823  funfni  6604  f1un  6800  fvelimab  6912  dff3  7052  fnex  7172  ralima  7192  f1cofveqaeq  7212  f1eqcocnv  7256  caofid0l  7664  caofid0r  7665  caofid1  7666  caofid2  7667  onmindif2  7761  limsssuc  7801  mptcnfimad  7939  fnse  8083  frrlem13  8248  iinon  8280  smoord  8305  smoword  8306  tfrlem11  8327  coflton  8607  cofonr  8610  naddasslem2  8631  boxcutc  8889  f1domg  8918  phpeqd  9146  ominf  9174  f1finf1o  9183  unfilem1  9215  f1opwfi  9266  marypha2  9352  supmax  9381  infmin  9409  ordtypelem6  9438  oiexg  9450  oien  9453  cantnff  9595  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  ttrcltr  9637  ttrclselem2  9647  opwf  9736  rankopb  9776  xpnum  9875  infxpenlem  9935  infxp  10136  cflim2  10185  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  ssfin3ds  10252  isf34lem5  10300  isf34lem6  10302  isfin1-3  10308  axcc3  10360  alephval2  10495  fpwwe2lem7  10560  canthp1  10577  tsken  10677  ltaddpr  10957  dedekind  11309  recextlem2  11781  recex  11782  gt0div  12022  ge0div  12023  lerec2  12044  uzwo2  12862  infssuzcl  12882  qmulcl  12917  xnegdi  13200  xmulpnf1n  13230  xadddi2  13249  fzm1  13561  2submod  13894  addmodlteq  13908  expnlbnd  14195  faclbnd5  14260  hasheni  14310  hashdifpr  14377  hashgt23el  14386  ccatrn  14552  ccatalpha  14556  swrds1  14629  swrdccat2  14632  ccatpfx  14663  swrdccatin2  14691  pfxccatin12lem2  14693  revccat  14728  revrev  14729  swrdco  14799  relexpindlem  15025  resqrex  15212  fzomaxdiflem  15305  climconst  15505  serf0  15643  fsumf1o  15685  fsumrev  15741  fsumabs  15764  cvgcmp  15779  binomlem  15794  isumshft  15804  climcndslem1  15814  climcndslem2  15815  climcnds  15816  supcvg  15821  fprodcl2lem  15915  tanneg  16115  rpnnen2lem11  16191  modm1div  16233  fzo0dvdseq  16292  bitsfzolem  16403  gcdcllem3  16470  hashdvds  16745  prmdivdiv  16757  reumodprminv  16775  nnnn0modprm0  16777  pythagtrip  16805  dvdsprmpweqle  16857  pockthg  16877  4sqlem9  16917  vdwmc2  16950  vdwlem2  16953  imasaddflem  17494  acsfn1  17627  acsfn1c  17628  acsfn2  17629  oppccofval  17682  rescabs  17800  diag2  18211  grpinvalem  18641  issubmnd  18729  imasmnd  18743  pwsco2mhm  18801  gsumwspan  18814  frmdss2  18831  grpinvssd  18993  pwssub  19030  imasgrp  19032  subginv  19109  subginvcl  19111  ecqusaddcl  19168  ghmpreima  19213  conjnsg  19229  gass  19276  gsmsymgreqlem2  19406  f1omvdmvd  19418  symgsssg  19442  symgfisg  19443  symgtrinv  19447  psgnunilem5  19469  sylow1lem2  19574  odcau  19579  sylow2a  19594  sylow2  19601  efgsp1  19712  frgpuptf  19745  frgpuptinv  19746  frgpupf  19748  frgpup3lem  19752  mulgdi  19801  gsumval3eu  19879  gsumzsplit  19902  gsumzmhm  19912  gsumxp2  19955  prdsgsum  19956  fsfnn0gsumfsffz  19958  ablfaclem3  20064  srgbinomlem  20211  gsummgp0  20297  pwsgprod  20309  imasring  20310  dvdsr01  20351  rngisom1  20446  01eq0ring  20507  issubrng2  20535  subrgcrng  20552  subrginv  20565  isdrngd  20742  imadrhmcl  20774  abv1z  20801  lcomfsupp  20897  lmodvneg1  20900  lspsn  20997  lmhmco  21038  lmhmima  21042  lmhmpreima  21043  reslmhm  21047  lbsextlem2  21157  isridlrng  21217  lidl0cl  21218  elrspsn  21238  rnglidlmmgm  21243  rnglidlmsgrp  21244  2idlcpblrng  21269  quscrng  21281  rngqiprngghmlem1  21285  rngqiprngghmlem3  21287  rngqiprnglinlem3  21291  rngqiprngimf1lem  21292  rngqiprngimf  21295  rng2idl1cntr  21303  znfld  21540  ipassr2  21627  ocvin  21654  pjfo  21695  obsne0  21705  frlmgsum  21752  aspval2  21878  psrlinv  21934  mplsubglem  21977  mpllsslem  21978  evlslem4  22054  evlslem1  22060  evlsval3  22067  mpfind  22093  evls1rhm  22287  madetsumid  22426  scmatcrng  22486  mdetleib2  22553  cramerimplem1  22648  m2pmfzgsumcl  22713  decpmatmul  22737  pmatcollpwscmat  22756  idpm2idmp  22766  pm2mpmhmlem1  22783  chpscmatgsummon  22810  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  topbas  22937  uncld  23006  incld  23008  elcls  23038  neiptopnei  23097  resttopon  23126  restdis  23143  cnclima  23233  paste  23259  cncmp  23357  clsconn  23395  conncompcld  23399  1stcfb  23410  2ndcsb  23414  2ndcredom  23415  kgencmp2  23511  txss12  23570  qtoptop2  23664  qtoptopon  23669  hmphindis  23762  uffixfr  23888  ufildr  23896  isfcls2  23978  tgplacthmeo  24068  tsmsgsum  24104  tgptsmscld  24116  tsmssplit  24117  ustuqtop5  24210  uspreg  24238  prdsxmetlem  24333  prdsbl  24456  metss  24473  metrest  24489  nrmmetd  24539  isngp2  24562  ngpsubcan  24579  lssnlm  24666  nmoid  24707  opnreen  24797  mpomulcn  24834  evth  24926  htpyco2  24946  phtpyco2  24957  clmvz  25078  tcphcph  25204  iscmet3  25260  metcld  25273  bcthlem2  25292  cssbn  25342  chlcsschl  25345  minveclem1  25391  evthicc2  25427  ovolunlem1a  25463  ovolicc2lem1  25484  ovolicc2lem4  25487  ovolicc2lem5  25488  uniioombllem2  25550  uniioombllem3  25552  vitalilem2  25576  vitalilem4  25578  vitalilem5  25579  itg2monolem1  25717  cpnres  25904  rolle  25957  dvlip2  25962  dvivthlem2  25976  dvfsumrlimge0  25997  deg1pwle  26085  plydivlem4  26262  ulm0  26356  efif1olem1  26506  efif1olem2  26507  eflogeq  26566  argimlt0  26577  logrec  26727  relogbcxp  26749  atanlogadd  26878  atanlogsub  26880  atantan  26887  ftalem4  27039  ftalem5  27040  basellem3  27046  chtub  27175  dchrpt  27230  dchrsum2  27231  gausslemma2dlem1a  27328  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2lgsoddprm  27379  dchrisumlem2  27453  pntrsumbnd2  27530  nosupbnd1lem4  27675  noinfbnd2lem1  27694  cutbdaylt  27790  oldlim  27879  madebday  27892  cofcutr  27916  addbday  28010  negbdaylem  28048  absmuls  28236  absnegs  28239  bdayfinlem  28478  cnvmot  28609  tglineneq  28712  midexlem  28760  midex  28805  axlowdimlem14  29024  uhgrspansubgrlem  29359  usgrres  29377  usgrnbcnvfv  29434  finsumvtxdg2sstep  29618  uspgr2wlkeq  29714  redwlk  29739  pthdivtx  29795  usgr2wlkspthlem2  29826  wwlknvtx  29913  2wlkdlem6  29999  umgr2wlkon  30018  rusgrnumwwlk  30046  clwwlkwwlksb  30124  clwwlknwwlksnb  30125  clwwnisshclwwsn  30129  clwwlknscsh  30132  clwlknf1oclwwlknlem1  30151  1wlkdlem2  30208  fusgreghash2wsp  30408  2clwwlklem  30413  2clwwlk2clwwlk  30420  numclwwlk6  30460  prssad  32599  prssbd  32600  ofrn2  32713  ofpreima2  32739  sgnval2  32808  argcj  32821  wrdsplex  32996  ccatf1  33009  mgcf1o  33063  gsumfs2d  33122  gsumhashmul  33128  gsummulsubdishift1  33129  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  cyc3co2  33201  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnsubrunlem1  33308  erler  33326  fracerl  33367  imaslmod  33413  elrspunidl  33488  qsidomlem1  33512  qsidomlem2  33513  ssdifidllem  33516  ssdifidlprm  33518  ressply1evls1  33625  ply1coedeg  33649  esplyfval3  33716  exsslsb  33741  dimpropd  33753  lbsdiflsp0  33770  extdg1id  33810  madjusmdetlem2  33972  zarcmplem  34025  eulerpartlemgvv  34520  boolesineq  34599  fineqvnttrclselem1  35265  vonf1owev  35290  pfxwlk  35306  revwlk  35307  pthhashvtx  35310  spthcycl  35311  umgracycusgr  35336  subfacp1lem5  35366  satfvsucsuc  35547  ply1divalg3  35824  weiunfrlem  36646  ttctr  36675  dfttc2g  36688  cnambfre  37989  mapdordlem2  42083  frlmvscadiccat  42951  ricdrng1  42973  evlsbagval  43002  0prjspn  43061  3cubes  43122  oninfint  43664  onexomgt  43669  onexoegt  43672  ordeldif  43686  oacl2g  43758  onmcl  43759  omabs2  43760  omcl2  43761  tfsconcatfv  43769  tfsconcatrev  43776  ofoafg  43782  ofoafo  43784  ofoaass  43788  ofoacom  43789  onsucunifi  43798  oaun3lem1  43802  oadif1lem  43807  oadif1  43808  naddwordnexlem4  43829  safesnsupfilb  43845  gneispace  44561  rr-phpd  44636  grumnudlem  44712  ax6e2ndeqALT  45357  sineq0ALT  45363  fnresdmss  45598  saliinclf  46754  hoicvr  46976  setsv  47838  sprsymrelfolem2  47953  lighneal  48074  indprmfz  48093  grimuhgr  48363  grimcnv  48364  uhgrimedgi  48366  uhgrimedg  48367  isuspgrim0lem  48369  isuspgrim0  48370  upgrimtrlslem1  48380  upgrimtrlslem2  48381  clnbgrgrim  48410  grimedg  48411  isubgr3stgrlem8  48449  clnbgr3stgrgrlim  48495  clnbgr3stgrgrlic  48496  lincresunit3  48957  2itscp  49257  resccat  49549