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  5097  axprlem4OLD  5376  brcogw  5825  funfni  6606  f1un  6802  fvelimab  6914  dff3  7054  fnex  7173  ralima  7193  f1cofveqaeq  7213  f1eqcocnv  7257  caofid0l  7665  caofid0r  7666  caofid1  7667  caofid2  7668  onmindif2  7762  limsssuc  7802  mptcnfimad  7940  fnse  8085  frrlem13  8250  iinon  8282  smoord  8307  smoword  8308  tfrlem11  8329  coflton  8609  cofonr  8612  naddasslem2  8633  boxcutc  8891  f1domg  8920  phpeqd  9148  ominf  9176  f1finf1o  9185  unfilem1  9217  f1opwfi  9268  marypha2  9354  supmax  9383  infmin  9411  ordtypelem6  9440  oiexg  9452  oien  9455  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  11308  recextlem2  11780  recex  11781  gt0div  12020  ge0div  12021  lerec2  12042  uzwo2  12837  infssuzcl  12857  qmulcl  12892  xnegdi  13175  xmulpnf1n  13205  xadddi2  13224  fzm1  13535  2submod  13867  addmodlteq  13881  expnlbnd  14168  faclbnd5  14233  hasheni  14283  hashdifpr  14350  hashgt23el  14359  ccatrn  14525  ccatalpha  14529  swrds1  14602  swrdccat2  14605  ccatpfx  14636  swrdccatin2  14664  pfxccatin12lem2  14666  revccat  14701  revrev  14702  swrdco  14772  relexpindlem  14998  resqrex  15185  fzomaxdiflem  15278  climconst  15478  serf0  15616  fsumf1o  15658  fsumrev  15714  fsumabs  15736  cvgcmp  15751  binomlem  15764  isumshft  15774  climcndslem1  15784  climcndslem2  15785  climcnds  15786  supcvg  15791  fprodcl2lem  15885  tanneg  16085  rpnnen2lem11  16161  modm1div  16203  fzo0dvdseq  16262  bitsfzolem  16373  gcdcllem3  16440  hashdvds  16714  prmdivdiv  16726  reumodprminv  16744  nnnn0modprm0  16746  pythagtrip  16774  dvdsprmpweqle  16826  pockthg  16846  4sqlem9  16886  vdwmc2  16919  vdwlem2  16922  imasaddflem  17463  acsfn1  17596  acsfn1c  17597  acsfn2  17598  oppccofval  17651  rescabs  17769  diag2  18180  grpinvalem  18610  issubmnd  18698  imasmnd  18712  pwsco2mhm  18770  gsumwspan  18783  frmdss2  18800  grpinvssd  18959  pwssub  18996  imasgrp  18998  subginv  19075  subginvcl  19077  ecqusaddcl  19134  ghmpreima  19179  conjnsg  19195  gass  19242  gsmsymgreqlem2  19372  f1omvdmvd  19384  symgsssg  19408  symgfisg  19409  symgtrinv  19413  psgnunilem5  19435  sylow1lem2  19540  odcau  19545  sylow2a  19560  sylow2  19567  efgsp1  19678  frgpuptf  19711  frgpuptinv  19712  frgpupf  19714  frgpup3lem  19718  mulgdi  19767  gsumval3eu  19845  gsumzsplit  19868  gsumzmhm  19878  gsumxp2  19921  prdsgsum  19922  fsfnn0gsumfsffz  19924  ablfaclem3  20030  srgbinomlem  20177  gsummgp0  20265  pwsgprod  20277  imasring  20278  dvdsr01  20319  rngisom1  20414  01eq0ring  20475  issubrng2  20503  subrgcrng  20520  subrginv  20533  isdrngd  20710  imadrhmcl  20742  abv1z  20769  lcomfsupp  20865  lmodvneg1  20868  lspsn  20965  lmhmco  21007  lmhmima  21011  lmhmpreima  21012  reslmhm  21016  lbsextlem2  21126  isridlrng  21186  lidl0cl  21187  elrspsn  21207  rnglidlmmgm  21212  rnglidlmsgrp  21213  2idlcpblrng  21238  quscrng  21250  rngqiprngghmlem1  21254  rngqiprngghmlem3  21256  rngqiprnglinlem3  21260  rngqiprngimf1lem  21261  rngqiprngimf  21264  rng2idl1cntr  21272  znfld  21527  ipassr2  21614  ocvin  21641  pjfo  21682  obsne0  21692  frlmgsum  21739  aspval2  21866  psrlinv  21923  mplsubglem  21966  mpllsslem  21967  evlslem4  22043  evlslem1  22049  evlsval3  22056  mpfind  22082  evls1rhm  22278  madetsumid  22417  scmatcrng  22477  mdetleib2  22544  cramerimplem1  22639  m2pmfzgsumcl  22704  decpmatmul  22728  pmatcollpwscmat  22747  idpm2idmp  22757  pm2mpmhmlem1  22774  chpscmatgsummon  22801  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  topbas  22928  uncld  22997  incld  22999  elcls  23029  neiptopnei  23088  resttopon  23117  restdis  23134  cnclima  23224  paste  23250  cncmp  23348  clsconn  23386  conncompcld  23390  1stcfb  23401  2ndcsb  23405  2ndcredom  23406  kgencmp2  23502  txss12  23561  qtoptop2  23655  qtoptopon  23660  hmphindis  23753  uffixfr  23879  ufildr  23887  isfcls2  23969  tgplacthmeo  24059  tsmsgsum  24095  tgptsmscld  24107  tsmssplit  24108  ustuqtop5  24201  uspreg  24229  prdsxmetlem  24324  prdsbl  24447  metss  24464  metrest  24480  nrmmetd  24530  isngp2  24553  ngpsubcan  24570  lssnlm  24657  nmoid  24698  opnreen  24788  mpomulcn  24826  evth  24926  htpyco2  24946  phtpyco2  24957  clmvz  25079  tcphcph  25205  iscmet3  25261  metcld  25274  bcthlem2  25293  cssbn  25343  chlcsschl  25346  minveclem1  25392  evthicc2  25429  ovolunlem1a  25465  ovolicc2lem1  25486  ovolicc2lem4  25489  ovolicc2lem5  25490  uniioombllem2  25552  uniioombllem3  25554  vitalilem2  25578  vitalilem4  25580  vitalilem5  25581  itg2monolem1  25719  cpnres  25907  rolle  25962  dvlip2  25968  dvivthlem2  25982  dvfsumrlimge0  26005  deg1pwle  26093  plydivlem4  26272  ulm0  26368  efif1olem1  26519  efif1olem2  26520  eflogeq  26579  argimlt0  26590  logrec  26741  relogbcxp  26763  atanlogadd  26892  atanlogsub  26894  atantan  26901  ftalem4  27054  ftalem5  27055  basellem3  27061  chtub  27191  dchrpt  27246  dchrsum2  27247  gausslemma2dlem1a  27344  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  2lgsoddprm  27395  dchrisumlem2  27469  pntrsumbnd2  27546  nosupbnd1lem4  27691  noinfbnd2lem1  27710  cutbdaylt  27806  oldlim  27895  madebday  27908  cofcutr  27932  addbday  28026  negbdaylem  28064  absmuls  28252  absnegs  28255  bdayfinlem  28494  cnvmot  28625  tglineneq  28728  midexlem  28776  midex  28821  axlowdimlem14  29040  uhgrspansubgrlem  29375  usgrres  29393  usgrnbcnvfv  29450  finsumvtxdg2sstep  29635  uspgr2wlkeq  29731  redwlk  29756  pthdivtx  29812  usgr2wlkspthlem2  29843  wwlknvtx  29930  2wlkdlem6  30016  umgr2wlkon  30035  rusgrnumwwlk  30063  clwwlkwwlksb  30141  clwwlknwwlksnb  30142  clwwnisshclwwsn  30146  clwwlknscsh  30149  clwlknf1oclwwlknlem1  30168  1wlkdlem2  30225  fusgreghash2wsp  30425  2clwwlklem  30430  2clwwlk2clwwlk  30437  numclwwlk6  30477  prssad  32615  prssbd  32616  ofrn2  32729  ofpreima2  32755  sgnval2  32824  argcj  32838  wrdsplex  33028  ccatf1  33041  mgcf1o  33095  gsumfs2d  33154  gsumhashmul  33160  gsummulsubdishift1  33161  cycpmco2lem5  33223  cycpmco2lem6  33224  cycpmco2lem7  33225  cycpmco2  33226  cyc3co2  33233  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnsubrunlem1  33340  erler  33358  fracerl  33399  imaslmod  33445  elrspunidl  33520  qsidomlem1  33544  qsidomlem2  33545  ssdifidllem  33548  ssdifidlprm  33550  ressply1evls1  33657  ply1coedeg  33681  esplyfval3  33748  exsslsb  33773  dimpropd  33785  lbsdiflsp0  33803  extdg1id  33843  madjusmdetlem2  34005  zarcmplem  34058  eulerpartlemgvv  34553  boolesineq  34632  fineqvnttrclselem1  35296  vonf1owev  35321  pfxwlk  35337  revwlk  35338  pthhashvtx  35341  spthcycl  35342  umgracycusgr  35367  subfacp1lem5  35397  satfvsucsuc  35578  ply1divalg3  35855  weiunfrlem  36677  cnambfre  37913  mapdordlem2  42007  frlmvscadiccat  42870  ricdrng1  42892  evlsbagval  42921  0prjspn  42980  3cubes  43041  oninfint  43587  onexomgt  43592  onexoegt  43595  ordeldif  43609  oacl2g  43681  onmcl  43682  omabs2  43683  omcl2  43684  tfsconcatfv  43692  tfsconcatrev  43699  ofoafg  43705  ofoafo  43707  ofoaass  43711  ofoacom  43712  onsucunifi  43721  oaun3lem1  43725  oadif1lem  43730  oadif1  43731  naddwordnexlem4  43752  safesnsupfilb  43768  gneispace  44484  rr-phpd  44559  grumnudlem  44635  ax6e2ndeqALT  45280  sineq0ALT  45286  fnresdmss  45521  saliinclf  46678  setsv  47732  sprsymrelfolem2  47847  lighneal  47965  grimuhgr  48241  grimcnv  48242  uhgrimedgi  48244  uhgrimedg  48245  isuspgrim0lem  48247  isuspgrim0  48248  upgrimtrlslem1  48258  upgrimtrlslem2  48259  clnbgrgrim  48288  grimedg  48289  isubgr3stgrlem8  48327  clnbgr3stgrgrlim  48373  clnbgr3stgrgrlic  48374  lincresunit3  48835  2itscp  49135  resccat  49427