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  5092  axprlem4OLD  5371  brcogw  5815  funfni  6592  f1un  6788  fvelimab  6899  dff3  7038  fnex  7157  ralima  7177  f1cofveqaeq  7198  f1eqcocnv  7242  caofid0l  7650  caofid0r  7651  caofid1  7652  caofid2  7653  onmindif2  7747  limsssuc  7790  mptcnfimad  7928  fnse  8073  frrlem13  8238  iinon  8270  smoord  8295  smoword  8296  tfrlem11  8317  coflton  8596  cofonr  8599  naddasslem2  8620  boxcutc  8875  f1domg  8904  phpeqd  9136  ominf  9163  f1finf1o  9174  findcard3OLD  9188  unfilem1  9212  f1opwfi  9265  marypha2  9348  supmax  9377  infmin  9405  ordtypelem6  9434  oiexg  9446  oien  9449  cantnff  9589  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1  9604  ttrcltr  9631  ttrclselem2  9641  opwf  9727  rankopb  9767  xpnum  9866  infxpenlem  9926  infxp  10127  cflim2  10176  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  ssfin3ds  10243  isf34lem5  10291  isf34lem6  10293  isfin1-3  10299  axcc3  10351  alephval2  10485  fpwwe2lem7  10550  canthp1  10567  tsken  10667  ltaddpr  10947  dedekind  11297  recextlem2  11769  recex  11770  gt0div  12009  ge0div  12010  lerec2  12031  uzwo2  12831  infssuzcl  12851  qmulcl  12886  xnegdi  13168  xmulpnf1n  13198  xadddi2  13217  fzm1  13528  2submod  13857  addmodlteq  13871  expnlbnd  14158  faclbnd5  14223  hasheni  14273  hashdifpr  14340  hashgt23el  14349  ccatrn  14514  ccatalpha  14518  swrds1  14591  swrdccat2  14594  ccatpfx  14625  swrdccatin2  14653  pfxccatin12lem2  14655  revccat  14690  revrev  14691  swrdco  14762  relexpindlem  14988  resqrex  15175  fzomaxdiflem  15268  climconst  15468  serf0  15606  fsumf1o  15648  fsumrev  15704  fsumabs  15726  cvgcmp  15741  binomlem  15754  isumshft  15764  climcndslem1  15774  climcndslem2  15775  climcnds  15776  supcvg  15781  fprodcl2lem  15875  tanneg  16075  rpnnen2lem11  16151  modm1div  16193  fzo0dvdseq  16252  bitsfzolem  16363  gcdcllem3  16430  hashdvds  16704  prmdivdiv  16716  reumodprminv  16734  nnnn0modprm0  16736  pythagtrip  16764  dvdsprmpweqle  16816  pockthg  16836  4sqlem9  16876  vdwmc2  16909  vdwlem2  16912  imasaddflem  17452  acsfn1  17585  acsfn1c  17586  acsfn2  17587  oppccofval  17640  rescabs  17758  diag2  18169  grpinvalem  18565  issubmnd  18653  imasmnd  18667  pwsco2mhm  18725  gsumwspan  18738  frmdss2  18755  grpinvssd  18914  pwssub  18951  imasgrp  18953  subginv  19030  subginvcl  19032  ecqusaddcl  19090  ghmpreima  19135  conjnsg  19151  gass  19198  gsmsymgreqlem2  19328  f1omvdmvd  19340  symgsssg  19364  symgfisg  19365  symgtrinv  19369  psgnunilem5  19391  sylow1lem2  19496  odcau  19501  sylow2a  19516  sylow2  19523  efgsp1  19634  frgpuptf  19667  frgpuptinv  19668  frgpupf  19670  frgpup3lem  19674  mulgdi  19723  gsumval3eu  19801  gsumzsplit  19824  gsumzmhm  19834  gsumxp2  19877  prdsgsum  19878  fsfnn0gsumfsffz  19880  ablfaclem3  19986  srgbinomlem  20133  gsummgp0  20221  imasring  20233  dvdsr01  20274  rngisom1  20369  01eq0ring  20433  issubrng2  20461  subrgcrng  20478  subrginv  20491  isdrngd  20668  imadrhmcl  20700  abv1z  20727  lcomfsupp  20823  lmodvneg1  20826  lspsn  20923  lmhmco  20965  lmhmima  20969  lmhmpreima  20970  reslmhm  20974  lbsextlem2  21084  isridlrng  21144  lidl0cl  21145  elrspsn  21165  rnglidlmmgm  21170  rnglidlmsgrp  21171  2idlcpblrng  21196  quscrng  21208  rngqiprngghmlem1  21212  rngqiprngghmlem3  21214  rngqiprnglinlem3  21218  rngqiprngimf1lem  21219  rngqiprngimf  21222  rng2idl1cntr  21230  znfld  21485  ipassr2  21572  ocvin  21599  pjfo  21640  obsne0  21650  frlmgsum  21697  aspval2  21823  psrlinv  21880  mplsubglem  21924  mpllsslem  21925  evlslem4  21999  evlslem1  22005  mpfind  22030  evls1rhm  22225  madetsumid  22364  scmatcrng  22424  mdetleib2  22491  cramerimplem1  22586  m2pmfzgsumcl  22651  decpmatmul  22675  pmatcollpwscmat  22694  idpm2idmp  22704  pm2mpmhmlem1  22721  chpscmatgsummon  22748  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  topbas  22875  uncld  22944  incld  22946  elcls  22976  neiptopnei  23035  resttopon  23064  restdis  23081  cnclima  23171  paste  23197  cncmp  23295  clsconn  23333  conncompcld  23337  1stcfb  23348  2ndcsb  23352  2ndcredom  23353  kgencmp2  23449  txss12  23508  qtoptop2  23602  qtoptopon  23607  hmphindis  23700  uffixfr  23826  ufildr  23834  isfcls2  23916  tgplacthmeo  24006  tsmsgsum  24042  tgptsmscld  24054  tsmssplit  24055  ustuqtop5  24149  uspreg  24177  prdsxmetlem  24272  prdsbl  24395  metss  24412  metrest  24428  nrmmetd  24478  isngp2  24501  ngpsubcan  24518  lssnlm  24605  nmoid  24646  opnreen  24736  mpomulcn  24774  evth  24874  htpyco2  24894  phtpyco2  24905  clmvz  25027  tcphcph  25153  iscmet3  25209  metcld  25222  bcthlem2  25241  cssbn  25291  chlcsschl  25294  minveclem1  25340  evthicc2  25377  ovolunlem1a  25413  ovolicc2lem1  25434  ovolicc2lem4  25437  ovolicc2lem5  25438  uniioombllem2  25500  uniioombllem3  25502  vitalilem2  25526  vitalilem4  25528  vitalilem5  25529  itg2monolem1  25667  cpnres  25855  rolle  25910  dvlip2  25916  dvivthlem2  25930  dvfsumrlimge0  25953  deg1pwle  26041  plydivlem4  26220  ulm0  26316  efif1olem1  26467  efif1olem2  26468  eflogeq  26527  argimlt0  26538  logrec  26689  relogbcxp  26711  atanlogadd  26840  atanlogsub  26842  atantan  26849  ftalem4  27002  ftalem5  27003  basellem3  27009  chtub  27139  dchrpt  27194  dchrsum2  27195  gausslemma2dlem1a  27292  2lgslem3a1  27327  2lgslem3b1  27328  2lgslem3c1  27329  2lgslem3d1  27330  2lgsoddprm  27343  dchrisumlem2  27417  pntrsumbnd2  27494  nosupbnd1lem4  27639  noinfbnd2lem1  27658  scutbdaylt  27747  oldlim  27819  madebday  27832  cofcutr  27855  addsbday  27947  negsbdaylem  27985  absmuls  28169  abssneg  28172  cnvmot  28504  tglineneq  28607  midexlem  28655  midex  28700  axlowdimlem14  28918  uhgrspansubgrlem  29253  usgrres  29271  usgrnbcnvfv  29328  finsumvtxdg2sstep  29513  uspgr2wlkeq  29609  redwlk  29634  pthdivtx  29690  usgr2wlkspthlem2  29721  wwlknvtx  29808  2wlkdlem6  29894  umgr2wlkon  29913  rusgrnumwwlk  29938  clwwlkwwlksb  30016  clwwlknwwlksnb  30017  clwwnisshclwwsn  30021  clwwlknscsh  30024  clwlknf1oclwwlknlem1  30043  1wlkdlem2  30100  fusgreghash2wsp  30300  2clwwlklem  30305  2clwwlk2clwwlk  30312  numclwwlk6  30352  prssad  32491  prssbd  32492  ofrn2  32597  ofpreima2  32623  sgnval2  32691  argcj  32705  wrdsplex  32890  ccatf1  32903  mgcf1o  32958  gsumfs2d  33021  gsumhashmul  33027  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmco2  33088  cyc3co2  33095  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnsubrunlem1  33197  erler  33215  fracerl  33255  imaslmod  33300  elrspunidl  33375  qsidomlem1  33399  qsidomlem2  33400  ssdifidllem  33403  ssdifidlprm  33405  ressply1evls1  33510  exsslsb  33568  dimpropd  33580  lbsdiflsp0  33598  extdg1id  33637  madjusmdetlem2  33794  zarcmplem  33847  eulerpartlemgvv  34343  boolesineq  34422  vonf1owev  35080  pfxwlk  35096  revwlk  35097  pthhashvtx  35100  spthcycl  35101  umgracycusgr  35126  subfacp1lem5  35156  satfvsucsuc  35337  ply1divalg3  35614  weiunfrlem  36437  cnambfre  37647  frlmvscadiccat  42479  ricdrng1  42501  pwsgprod  42517  evlsval3  42532  evlsbagval  42539  0prjspn  42601  3cubes  42663  oninfint  43209  onexomgt  43214  onexoegt  43217  ordeldif  43231  oacl2g  43303  onmcl  43304  omabs2  43305  omcl2  43306  tfsconcatfv  43314  tfsconcatrev  43321  ofoafg  43327  ofoafo  43329  ofoaass  43333  ofoacom  43334  onsucunifi  43343  oaun3lem1  43347  oadif1lem  43352  oadif1  43353  naddwordnexlem4  43374  safesnsupfilb  43391  gneispace  44107  rr-phpd  44182  grumnudlem  44258  ax6e2ndeqALT  44904  sineq0ALT  44910  fnresdmss  45146  saliinclf  46308  setsv  47363  sprsymrelfolem2  47478  lighneal  47596  grimuhgr  47872  grimcnv  47873  uhgrimedgi  47875  uhgrimedg  47876  isuspgrim0lem  47878  isuspgrim0  47879  upgrimtrlslem1  47889  upgrimtrlslem2  47890  clnbgrgrim  47919  grimedg  47920  isubgr3stgrlem8  47958  clnbgr3stgrgrlim  48004  clnbgr3stgrgrlic  48005  lincresunit3  48467  2itscp  48767  resccat  49060