Theorem syl2an2r 685

Description: syl2anr 597 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 580	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 591	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  5095  axprlem4OLD  5374  brcogw  5817  funfni  6598  f1un  6794  fvelimab  6906  dff3  7045  fnex  7163  ralima  7183  f1cofveqaeq  7203  f1eqcocnv  7247  caofid0l  7655  caofid0r  7656  caofid1  7657  caofid2  7658  onmindif2  7752  limsssuc  7792  mptcnfimad  7930  fnse  8075  frrlem13  8240  iinon  8272  smoord  8297  smoword  8298  tfrlem11  8319  coflton  8599  cofonr  8602  naddasslem2  8623  boxcutc  8879  f1domg  8908  phpeqd  9136  ominf  9164  f1finf1o  9173  unfilem1  9205  f1opwfi  9256  marypha2  9342  supmax  9371  infmin  9399  ordtypelem6  9428  oiexg  9440  oien  9443  cantnff  9583  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1  9598  ttrcltr  9625  ttrclselem2  9635  opwf  9724  rankopb  9764  xpnum  9863  infxpenlem  9923  infxp  10124  cflim2  10173  cofsmo  10179  cfsmolem  10180  cfcoflem  10182  ssfin3ds  10240  isf34lem5  10288  isf34lem6  10290  isfin1-3  10296  axcc3  10348  alephval2  10483  fpwwe2lem7  10548  canthp1  10565  tsken  10665  ltaddpr  10945  dedekind  11296  recextlem2  11768  recex  11769  gt0div  12008  ge0div  12009  lerec2  12030  uzwo2  12825  infssuzcl  12845  qmulcl  12880  xnegdi  13163  xmulpnf1n  13193  xadddi2  13212  fzm1  13523  2submod  13855  addmodlteq  13869  expnlbnd  14156  faclbnd5  14221  hasheni  14271  hashdifpr  14338  hashgt23el  14347  ccatrn  14513  ccatalpha  14517  swrds1  14590  swrdccat2  14593  ccatpfx  14624  swrdccatin2  14652  pfxccatin12lem2  14654  revccat  14689  revrev  14690  swrdco  14760  relexpindlem  14986  resqrex  15173  fzomaxdiflem  15266  climconst  15466  serf0  15604  fsumf1o  15646  fsumrev  15702  fsumabs  15724  cvgcmp  15739  binomlem  15752  isumshft  15762  climcndslem1  15772  climcndslem2  15773  climcnds  15774  supcvg  15779  fprodcl2lem  15873  tanneg  16073  rpnnen2lem11  16149  modm1div  16191  fzo0dvdseq  16250  bitsfzolem  16361  gcdcllem3  16428  hashdvds  16702  prmdivdiv  16714  reumodprminv  16732  nnnn0modprm0  16734  pythagtrip  16762  dvdsprmpweqle  16814  pockthg  16834  4sqlem9  16874  vdwmc2  16907  vdwlem2  16910  imasaddflem  17451  acsfn1  17584  acsfn1c  17585  acsfn2  17586  oppccofval  17639  rescabs  17757  diag2  18168  grpinvalem  18598  issubmnd  18686  imasmnd  18700  pwsco2mhm  18758  gsumwspan  18771  frmdss2  18788  grpinvssd  18947  pwssub  18984  imasgrp  18986  subginv  19063  subginvcl  19065  ecqusaddcl  19122  ghmpreima  19167  conjnsg  19183  gass  19230  gsmsymgreqlem2  19360  f1omvdmvd  19372  symgsssg  19396  symgfisg  19397  symgtrinv  19401  psgnunilem5  19423  sylow1lem2  19528  odcau  19533  sylow2a  19548  sylow2  19555  efgsp1  19666  frgpuptf  19699  frgpuptinv  19700  frgpupf  19702  frgpup3lem  19706  mulgdi  19755  gsumval3eu  19833  gsumzsplit  19856  gsumzmhm  19866  gsumxp2  19909  prdsgsum  19910  fsfnn0gsumfsffz  19912  ablfaclem3  20018  srgbinomlem  20165  gsummgp0  20253  pwsgprod  20265  imasring  20266  dvdsr01  20307  rngisom1  20402  01eq0ring  20463  issubrng2  20491  subrgcrng  20508  subrginv  20521  isdrngd  20698  imadrhmcl  20730  abv1z  20757  lcomfsupp  20853  lmodvneg1  20856  lspsn  20953  lmhmco  20995  lmhmima  20999  lmhmpreima  21000  reslmhm  21004  lbsextlem2  21114  isridlrng  21174  lidl0cl  21175  elrspsn  21195  rnglidlmmgm  21200  rnglidlmsgrp  21201  2idlcpblrng  21226  quscrng  21238  rngqiprngghmlem1  21242  rngqiprngghmlem3  21244  rngqiprnglinlem3  21248  rngqiprngimf1lem  21249  rngqiprngimf  21252  rng2idl1cntr  21260  znfld  21515  ipassr2  21602  ocvin  21629  pjfo  21670  obsne0  21680  frlmgsum  21727  aspval2  21854  psrlinv  21911  mplsubglem  21954  mpllsslem  21955  evlslem4  22031  evlslem1  22037  evlsval3  22044  mpfind  22070  evls1rhm  22266  madetsumid  22405  scmatcrng  22465  mdetleib2  22532  cramerimplem1  22627  m2pmfzgsumcl  22692  decpmatmul  22716  pmatcollpwscmat  22735  idpm2idmp  22745  pm2mpmhmlem1  22762  chpscmatgsummon  22789  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  topbas  22916  uncld  22985  incld  22987  elcls  23017  neiptopnei  23076  resttopon  23105  restdis  23122  cnclima  23212  paste  23238  cncmp  23336  clsconn  23374  conncompcld  23378  1stcfb  23389  2ndcsb  23393  2ndcredom  23394  kgencmp2  23490  txss12  23549  qtoptop2  23643  qtoptopon  23648  hmphindis  23741  uffixfr  23867  ufildr  23875  isfcls2  23957  tgplacthmeo  24047  tsmsgsum  24083  tgptsmscld  24095  tsmssplit  24096  ustuqtop5  24189  uspreg  24217  prdsxmetlem  24312  prdsbl  24435  metss  24452  metrest  24468  nrmmetd  24518  isngp2  24541  ngpsubcan  24558  lssnlm  24645  nmoid  24686  opnreen  24776  mpomulcn  24814  evth  24914  htpyco2  24934  phtpyco2  24945  clmvz  25067  tcphcph  25193  iscmet3  25249  metcld  25262  bcthlem2  25281  cssbn  25331  chlcsschl  25334  minveclem1  25380  evthicc2  25417  ovolunlem1a  25453  ovolicc2lem1  25474  ovolicc2lem4  25477  ovolicc2lem5  25478  uniioombllem2  25540  uniioombllem3  25542  vitalilem2  25566  vitalilem4  25568  vitalilem5  25569  itg2monolem1  25707  cpnres  25895  rolle  25950  dvlip2  25956  dvivthlem2  25970  dvfsumrlimge0  25993  deg1pwle  26081  plydivlem4  26260  ulm0  26356  efif1olem1  26507  efif1olem2  26508  eflogeq  26567  argimlt0  26578  logrec  26729  relogbcxp  26751  atanlogadd  26880  atanlogsub  26882  atantan  26889  ftalem4  27042  ftalem5  27043  basellem3  27049  chtub  27179  dchrpt  27234  dchrsum2  27235  gausslemma2dlem1a  27332  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2lgsoddprm  27383  dchrisumlem2  27457  pntrsumbnd2  27534  nosupbnd1lem4  27679  noinfbnd2lem1  27698  cutbdaylt  27794  oldlim  27883  madebday  27896  cofcutr  27920  addbday  28014  negbdaylem  28052  absmuls  28240  absnegs  28243  bdayfinlem  28482  cnvmot  28613  tglineneq  28716  midexlem  28764  midex  28809  axlowdimlem14  29028  uhgrspansubgrlem  29363  usgrres  29381  usgrnbcnvfv  29438  finsumvtxdg2sstep  29623  uspgr2wlkeq  29719  redwlk  29744  pthdivtx  29800  usgr2wlkspthlem2  29831  wwlknvtx  29918  2wlkdlem6  30004  umgr2wlkon  30023  rusgrnumwwlk  30051  clwwlkwwlksb  30129  clwwlknwwlksnb  30130  clwwnisshclwwsn  30134  clwwlknscsh  30137  clwlknf1oclwwlknlem1  30156  1wlkdlem2  30213  fusgreghash2wsp  30413  2clwwlklem  30418  2clwwlk2clwwlk  30425  numclwwlk6  30465  prssad  32604  prssbd  32605  ofrn2  32718  ofpreima2  32744  sgnval2  32814  argcj  32828  wrdsplex  33018  ccatf1  33031  mgcf1o  33085  gsumfs2d  33144  gsumhashmul  33150  gsummulsubdishift1  33151  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cyc3co2  33222  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnsubrunlem1  33329  erler  33347  fracerl  33388  imaslmod  33434  elrspunidl  33509  qsidomlem1  33533  qsidomlem2  33534  ssdifidllem  33537  ssdifidlprm  33539  ressply1evls1  33646  ply1coedeg  33670  esplyfval3  33730  exsslsb  33753  dimpropd  33765  lbsdiflsp0  33783  extdg1id  33823  madjusmdetlem2  33985  zarcmplem  34038  eulerpartlemgvv  34533  boolesineq  34612  fineqvnttrclselem1  35277  vonf1owev  35302  pfxwlk  35318  revwlk  35319  pthhashvtx  35322  spthcycl  35323  umgracycusgr  35348  subfacp1lem5  35378  satfvsucsuc  35559  ply1divalg3  35836  weiunfrlem  36658  cnambfre  37865  mapdordlem2  41893  frlmvscadiccat  42757  ricdrng1  42779  evlsbagval  42808  0prjspn  42867  3cubes  42928  oninfint  43474  onexomgt  43479  onexoegt  43482  ordeldif  43496  oacl2g  43568  onmcl  43569  omabs2  43570  omcl2  43571  tfsconcatfv  43579  tfsconcatrev  43586  ofoafg  43592  ofoafo  43594  ofoaass  43598  ofoacom  43599  onsucunifi  43608  oaun3lem1  43612  oadif1lem  43617  oadif1  43618  naddwordnexlem4  43639  safesnsupfilb  43655  gneispace  44371  rr-phpd  44446  grumnudlem  44522  ax6e2ndeqALT  45167  sineq0ALT  45173  fnresdmss  45408  saliinclf  46566  setsv  47620  sprsymrelfolem2  47735  lighneal  47853  grimuhgr  48129  grimcnv  48130  uhgrimedgi  48132  uhgrimedg  48133  isuspgrim0lem  48135  isuspgrim0  48136  upgrimtrlslem1  48146  upgrimtrlslem2  48147  clnbgrgrim  48176  grimedg  48177  isubgr3stgrlem8  48215  clnbgr3stgrgrlim  48261  clnbgr3stgrgrlic  48262  lincresunit3  48723  2itscp  49023  resccat  49315