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  5088  axprlem4OLD  5367  brcogw  5808  funfni  6587  f1un  6783  fvelimab  6894  dff3  7033  fnex  7151  ralima  7171  f1cofveqaeq  7191  f1eqcocnv  7235  caofid0l  7643  caofid0r  7644  caofid1  7645  caofid2  7646  onmindif2  7740  limsssuc  7780  mptcnfimad  7918  fnse  8063  frrlem13  8228  iinon  8260  smoord  8285  smoword  8286  tfrlem11  8307  coflton  8586  cofonr  8589  naddasslem2  8610  boxcutc  8865  f1domg  8894  phpeqd  9121  ominf  9148  f1finf1o  9157  unfilem1  9189  f1opwfi  9240  marypha2  9323  supmax  9352  infmin  9380  ordtypelem6  9409  oiexg  9421  oien  9424  cantnff  9564  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1  9579  ttrcltr  9606  ttrclselem2  9616  opwf  9702  rankopb  9742  xpnum  9841  infxpenlem  9901  infxp  10102  cflim2  10151  cofsmo  10157  cfsmolem  10158  cfcoflem  10160  ssfin3ds  10218  isf34lem5  10266  isf34lem6  10268  isfin1-3  10274  axcc3  10326  alephval2  10460  fpwwe2lem7  10525  canthp1  10542  tsken  10642  ltaddpr  10922  dedekind  11273  recextlem2  11745  recex  11746  gt0div  11985  ge0div  11986  lerec2  12007  uzwo2  12807  infssuzcl  12827  qmulcl  12862  xnegdi  13144  xmulpnf1n  13174  xadddi2  13193  fzm1  13504  2submod  13836  addmodlteq  13850  expnlbnd  14137  faclbnd5  14202  hasheni  14252  hashdifpr  14319  hashgt23el  14328  ccatrn  14494  ccatalpha  14498  swrds1  14571  swrdccat2  14574  ccatpfx  14605  swrdccatin2  14633  pfxccatin12lem2  14635  revccat  14670  revrev  14671  swrdco  14741  relexpindlem  14967  resqrex  15154  fzomaxdiflem  15247  climconst  15447  serf0  15585  fsumf1o  15627  fsumrev  15683  fsumabs  15705  cvgcmp  15720  binomlem  15733  isumshft  15743  climcndslem1  15753  climcndslem2  15754  climcnds  15755  supcvg  15760  fprodcl2lem  15854  tanneg  16054  rpnnen2lem11  16130  modm1div  16172  fzo0dvdseq  16231  bitsfzolem  16342  gcdcllem3  16409  hashdvds  16683  prmdivdiv  16695  reumodprminv  16713  nnnn0modprm0  16715  pythagtrip  16743  dvdsprmpweqle  16795  pockthg  16815  4sqlem9  16855  vdwmc2  16888  vdwlem2  16891  imasaddflem  17431  acsfn1  17564  acsfn1c  17565  acsfn2  17566  oppccofval  17619  rescabs  17737  diag2  18148  grpinvalem  18578  issubmnd  18666  imasmnd  18680  pwsco2mhm  18738  gsumwspan  18751  frmdss2  18768  grpinvssd  18927  pwssub  18964  imasgrp  18966  subginv  19043  subginvcl  19045  ecqusaddcl  19103  ghmpreima  19148  conjnsg  19164  gass  19211  gsmsymgreqlem2  19341  f1omvdmvd  19353  symgsssg  19377  symgfisg  19378  symgtrinv  19382  psgnunilem5  19404  sylow1lem2  19509  odcau  19514  sylow2a  19529  sylow2  19536  efgsp1  19647  frgpuptf  19680  frgpuptinv  19681  frgpupf  19683  frgpup3lem  19687  mulgdi  19736  gsumval3eu  19814  gsumzsplit  19837  gsumzmhm  19847  gsumxp2  19890  prdsgsum  19891  fsfnn0gsumfsffz  19893  ablfaclem3  19999  srgbinomlem  20146  gsummgp0  20234  imasring  20246  dvdsr01  20287  rngisom1  20382  01eq0ring  20443  issubrng2  20471  subrgcrng  20488  subrginv  20501  isdrngd  20678  imadrhmcl  20710  abv1z  20737  lcomfsupp  20833  lmodvneg1  20836  lspsn  20933  lmhmco  20975  lmhmima  20979  lmhmpreima  20980  reslmhm  20984  lbsextlem2  21094  isridlrng  21154  lidl0cl  21155  elrspsn  21175  rnglidlmmgm  21180  rnglidlmsgrp  21181  2idlcpblrng  21206  quscrng  21218  rngqiprngghmlem1  21222  rngqiprngghmlem3  21224  rngqiprnglinlem3  21228  rngqiprngimf1lem  21229  rngqiprngimf  21232  rng2idl1cntr  21240  znfld  21495  ipassr2  21582  ocvin  21609  pjfo  21650  obsne0  21660  frlmgsum  21707  aspval2  21833  psrlinv  21890  mplsubglem  21934  mpllsslem  21935  evlslem4  22009  evlslem1  22015  mpfind  22040  evls1rhm  22235  madetsumid  22374  scmatcrng  22434  mdetleib2  22501  cramerimplem1  22596  m2pmfzgsumcl  22661  decpmatmul  22685  pmatcollpwscmat  22704  idpm2idmp  22714  pm2mpmhmlem1  22731  chpscmatgsummon  22758  chfacfscmulgsum  22773  chfacfpmmulgsum  22777  topbas  22885  uncld  22954  incld  22956  elcls  22986  neiptopnei  23045  resttopon  23074  restdis  23091  cnclima  23181  paste  23207  cncmp  23305  clsconn  23343  conncompcld  23347  1stcfb  23358  2ndcsb  23362  2ndcredom  23363  kgencmp2  23459  txss12  23518  qtoptop2  23612  qtoptopon  23617  hmphindis  23710  uffixfr  23836  ufildr  23844  isfcls2  23926  tgplacthmeo  24016  tsmsgsum  24052  tgptsmscld  24064  tsmssplit  24065  ustuqtop5  24158  uspreg  24186  prdsxmetlem  24281  prdsbl  24404  metss  24421  metrest  24437  nrmmetd  24487  isngp2  24510  ngpsubcan  24527  lssnlm  24614  nmoid  24655  opnreen  24745  mpomulcn  24783  evth  24883  htpyco2  24903  phtpyco2  24914  clmvz  25036  tcphcph  25162  iscmet3  25218  metcld  25231  bcthlem2  25250  cssbn  25300  chlcsschl  25303  minveclem1  25349  evthicc2  25386  ovolunlem1a  25422  ovolicc2lem1  25443  ovolicc2lem4  25446  ovolicc2lem5  25447  uniioombllem2  25509  uniioombllem3  25511  vitalilem2  25535  vitalilem4  25537  vitalilem5  25538  itg2monolem1  25676  cpnres  25864  rolle  25919  dvlip2  25925  dvivthlem2  25939  dvfsumrlimge0  25962  deg1pwle  26050  plydivlem4  26229  ulm0  26325  efif1olem1  26476  efif1olem2  26477  eflogeq  26536  argimlt0  26547  logrec  26698  relogbcxp  26720  atanlogadd  26849  atanlogsub  26851  atantan  26858  ftalem4  27011  ftalem5  27012  basellem3  27018  chtub  27148  dchrpt  27203  dchrsum2  27204  gausslemma2dlem1a  27301  2lgslem3a1  27336  2lgslem3b1  27337  2lgslem3c1  27338  2lgslem3d1  27339  2lgsoddprm  27352  dchrisumlem2  27426  pntrsumbnd2  27503  nosupbnd1lem4  27648  noinfbnd2lem1  27667  scutbdaylt  27757  oldlim  27830  madebday  27843  cofcutr  27866  addsbday  27958  negsbdaylem  27996  absmuls  28180  abssneg  28183  cnvmot  28517  tglineneq  28620  midexlem  28668  midex  28713  axlowdimlem14  28931  uhgrspansubgrlem  29266  usgrres  29284  usgrnbcnvfv  29341  finsumvtxdg2sstep  29526  uspgr2wlkeq  29622  redwlk  29647  pthdivtx  29703  usgr2wlkspthlem2  29734  wwlknvtx  29821  2wlkdlem6  29907  umgr2wlkon  29926  rusgrnumwwlk  29951  clwwlkwwlksb  30029  clwwlknwwlksnb  30030  clwwnisshclwwsn  30034  clwwlknscsh  30037  clwlknf1oclwwlknlem1  30056  1wlkdlem2  30113  fusgreghash2wsp  30313  2clwwlklem  30318  2clwwlk2clwwlk  30325  numclwwlk6  30365  prssad  32504  prssbd  32505  ofrn2  32617  ofpreima2  32643  sgnval2  32713  argcj  32727  wrdsplex  32912  ccatf1  32925  mgcf1o  32979  gsumfs2d  33030  gsumhashmul  33036  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cyc3co2  33104  elrgspnlem1  33204  elrgspnlem2  33205  elrgspnsubrunlem1  33209  erler  33227  fracerl  33267  imaslmod  33313  elrspunidl  33388  qsidomlem1  33412  qsidomlem2  33413  ssdifidllem  33416  ssdifidlprm  33418  ressply1evls1  33523  exsslsb  33604  dimpropd  33616  lbsdiflsp0  33634  extdg1id  33674  madjusmdetlem2  33836  zarcmplem  33889  eulerpartlemgvv  34384  boolesineq  34463  fineqvnttrclselem1  35129  vonf1owev  35140  pfxwlk  35156  revwlk  35157  pthhashvtx  35160  spthcycl  35161  umgracycusgr  35186  subfacp1lem5  35216  satfvsucsuc  35397  ply1divalg3  35674  weiunfrlem  36497  cnambfre  37707  frlmvscadiccat  42538  ricdrng1  42560  pwsgprod  42576  evlsval3  42591  evlsbagval  42598  0prjspn  42660  3cubes  42722  oninfint  43268  onexomgt  43273  onexoegt  43276  ordeldif  43290  oacl2g  43362  onmcl  43363  omabs2  43364  omcl2  43365  tfsconcatfv  43373  tfsconcatrev  43380  ofoafg  43386  ofoafo  43388  ofoaass  43392  ofoacom  43393  onsucunifi  43402  oaun3lem1  43406  oadif1lem  43411  oadif1  43412  naddwordnexlem4  43433  safesnsupfilb  43450  gneispace  44166  rr-phpd  44241  grumnudlem  44317  ax6e2ndeqALT  44962  sineq0ALT  44968  fnresdmss  45204  saliinclf  46363  setsv  47408  sprsymrelfolem2  47523  lighneal  47641  grimuhgr  47917  grimcnv  47918  uhgrimedgi  47920  uhgrimedg  47921  isuspgrim0lem  47923  isuspgrim0  47924  upgrimtrlslem1  47934  upgrimtrlslem2  47935  clnbgrgrim  47964  grimedg  47965  isubgr3stgrlem8  48003  clnbgr3stgrgrlim  48049  clnbgr3stgrgrlic  48050  lincresunit3  48512  2itscp  48812  resccat  49105