Theorem syl2an2r 697

Description: syl2anr 608 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 591	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 602	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5102  axprlem4OLD  5392  brcogw  5845  funfni  6631  f1un  6831  fvelimab  6943  dff3  7085  fnex  7205  ralima  7225  f1cofveqaeq  7245  f1eqcocnv  7289  caofid0l  7697  caofid0r  7698  caofid1  7699  caofid2  7700  onmindif2  7794  limsssuc  7834  mptcnfimad  7971  fnse  8117  frrlem13  8283  iinon  8315  smoord  8340  smoword  8341  tfrlem11  8363  coflton  8645  cofonr  8648  naddasslem2  8670  boxcutc  8927  f1domg  8956  phpeqd  9184  ominf  9212  f1finf1o  9221  unfilem1  9253  f1opwfi  9301  marypha2  9387  supmax  9416  infmin  9444  ordtypelem6  9473  oiexg  9485  oien  9488  cantnff  9631  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1  9646  ttrcltr  9673  ttrclselem2  9683  opwf  9772  rankopb  9812  xpnum  9925  infxpenlem  9985  infxp  10185  cflim2  10235  cofsmo  10241  cfsmolem  10242  cfcoflem  10244  ssfin3ds  10302  isf34lem5  10350  isf34lem6  10352  isfin1-3  10358  axcc3  10410  alephval2  10545  fpwwe2lem7  10610  canthp1  10627  tsken  10727  ltaddpr  11007  dedekind  11361  recextlem2  11833  recex  11834  gt0div  12072  ge0div  12073  lerec2  12094  uzwo2  12927  infssuzcl  12947  qmulcl  12982  xnegdi  13265  xmulpnf1n  13295  xadddi2  13314  fzm1  13626  2submod  13959  addmodlteq  13973  expnlbnd  14260  faclbnd5  14325  hasheni  14375  hashdifpr  14442  hashgt23el  14451  ccatrn  14617  ccatalpha  14621  swrds1  14694  swrdccat2  14697  ccatpfx  14728  swrdccatin2  14756  pfxccatin12lem2  14758  revccat  14793  revrev  14794  swrdco  14864  relexpindlem  15090  resqrex  15291  fzomaxdiflem  15384  climconst  15584  serf0  15722  fsumf1o  15764  fsumrev  15820  fsumabs  15843  cvgcmp  15858  binomlem  15873  isumshft  15883  climcndslem1  15893  climcndslem2  15894  climcnds  15895  supcvg  15900  fprodcl2lem  15994  tanneg  16194  rpnnen2lem11  16270  modm1div  16312  fzo0dvdseq  16371  bitsfzolem  16482  gcdcllem3  16549  hashdvds  16824  prmdivdiv  16836  reumodprminv  16854  nnnn0modprm0  16856  pythagtrip  16884  dvdsprmpweqle  16936  pockthg  16956  4sqlem9  16996  vdwmc2  17029  vdwlem2  17032  imasaddflem  17574  acsfn1  17707  acsfn1c  17708  acsfn2  17709  oppccofval  17762  rescabs  17880  diag2  18291  grpinvalem  18721  issubmnd  18809  imasmnd  18823  pwsco2mhm  18882  gsumwspan  18895  frmdss2  18912  grpinvssd  19074  pwssub  19111  imasgrp  19113  subginv  19190  subginvcl  19192  ecqusaddcl  19255  ghmpreima  19299  conjnsg  19315  gass  19362  gsmsymgreqlem2  19492  f1omvdmvd  19504  symgsssg  19528  symgfisg  19529  symgtrinv  19533  psgnunilem5  19555  sylow1lem2  19660  odcau  19665  sylow2a  19680  sylow2  19687  efgsp1  19798  frgpuptf  19831  frgpuptinv  19832  frgpupf  19834  frgpup3lem  19838  mulgdi  19887  gsumval3eu  19965  gsumzsplit  19988  gsumzmhm  19998  gsumxp2  20041  prdsgsum  20042  fsfnn0gsumfsffz  20044  ablfaclem3  20150  srgbinomlem  20303  gsummgp0  20390  pwsgprod  20402  imasring  20403  dvdsr01  20444  rngisom1  20539  01eq0ring  20605  issubrng2  20634  subrgcrng  20651  subrginv  20664  isdrngd  20838  imadrhmcl  20869  abv1z  20896  lcomfsupp  20992  lmodvneg1  20995  lspsn  21092  lmhmco  21133  lmhmima  21137  lmhmpreima  21138  reslmhm  21142  lbsextlem2  21252  isridlrng  21313  lidl0cl  21314  lidlunin0  21330  elrspsn  21338  rnglidlmmgm  21344  rnglidlmsgrp  21345  2idlcpblrng  21372  quscrng  21385  rngqiprngghmlem1  21389  rngqiprngghmlem3  21391  rngqiprnglinlem3  21395  rngqiprngimf1lem  21396  rngqiprngimf  21399  rng2idl1cntr  21407  qsidomlem1  21440  qsidomlem2  21441  ssdifidllem  21444  ssdifidlprm  21446  znfld  21670  ipassr2  21757  ocvin  21784  pjfo  21825  obsne0  21835  frlmgsum  21882  aspval2  22008  psrlinv  22065  mplsubglem  22108  mpllsslem  22109  evlslem4  22187  evlslem1  22193  evlsval3  22200  mpfind  22226  evls1rhm  22443  madetsumid  22579  scmatcrng  22639  mdetleib2  22706  cramerimplem1  22801  m2pmfzgsumcl  22866  decpmatmul  22890  pmatcollpwscmat  22909  idpm2idmp  22919  pm2mpmhmlem1  22936  chpscmatgsummon  22963  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  topbas  23090  uncld  23159  incld  23161  elcls  23191  neiptopnei  23250  resttopon  23279  restdis  23296  cnclima  23386  paste  23412  cncmp  23510  clsconn  23548  conncompcld  23552  1stcfb  23563  2ndcsb  23567  2ndcredom  23568  kgencmp2  23664  txss12  23723  qtoptop2  23817  qtoptopon  23822  hmphindis  23915  uffixfr  24041  ufildr  24049  isfcls2  24131  tgplacthmeo  24221  tsmsgsum  24257  tgptsmscld  24269  tsmssplit  24270  ustuqtop5  24363  uspreg  24391  prdsxmetlem  24486  prdsbl  24609  metss  24626  metrest  24642  nrmmetd  24692  isngp2  24715  ngpsubcan  24732  lssnlm  24819  nmoid  24860  opnreen  24950  mpomulcn  24987  evth  25079  htpyco2  25099  phtpyco2  25110  clmvz  25231  tcphcph  25357  iscmet3  25413  metcld  25426  bcthlem2  25445  cssbn  25495  chlcsschl  25498  minveclem1  25544  evthicc2  25580  ovolunlem1a  25616  ovolicc2lem1  25637  ovolicc2lem4  25640  ovolicc2lem5  25641  uniioombllem2  25703  uniioombllem3  25705  vitalilem2  25729  vitalilem4  25731  vitalilem5  25732  itg2monolem1  25870  cpnres  26057  rolle  26110  dvlip2  26115  dvivthlem2  26129  dvfsumrlimge0  26150  deg1pwle  26238  plydivlem4  26418  ulm0  26512  efif1olem1  26665  efif1olem2  26666  eflogeq  26725  argimlt0  26736  logrec  26886  relogbcxp  26908  atanlogadd  27037  atanlogsub  27039  atantan  27046  ftalem4  27198  ftalem5  27199  basellem3  27205  chtub  27334  dchrpt  27389  dchrsum2  27390  gausslemma2dlem1a  27487  2lgslem3a1  27522  2lgslem3b1  27523  2lgslem3c1  27524  2lgslem3d1  27525  2lgsoddprm  27538  dchrisumlem2  27612  pntrsumbnd2  27689  nosupbnd1lem4  27833  noinfbnd2lem1  27852  cutbdaylt  27949  oldlim  28038  madebday  28051  cofcutr  28075  addbday  28169  negbdaylem  28207  absmuls  28395  absnegs  28398  bdayfinlem  28637  cnvmot  28768  tglineneq  28872  midexlem  28923  midex  28968  plngrotlem1  29017  axlowdimlem14  29214  uhgrspansubgrlem  29549  usgrres  29567  usgrnbcnvfv  29624  finsumvtxdg2sstep  29808  uspgr2wlkeq  29904  redwlk  29929  pthdivtx  29985  usgr2wlkspthlem2  30016  wwlknvtx  30103  2wlkdlem6  30189  umgr2wlkon  30208  rusgrnumwwlk  30236  clwwlkwwlksb  30314  clwwlknwwlksnb  30315  clwwnisshclwwsn  30319  clwwlknscsh  30322  clwlknf1oclwwlknlem1  30341  1wlkdlem2  30398  fusgreghash2wsp  30598  2clwwlklem  30603  2clwwlk2clwwlk  30610  numclwwlk6  30650  prssad  32785  prssbd  32786  ofrn2  32897  ofpreima2  32923  sgnval2  32992  argcj  33005  wrdsplex  33169  ccatf1  33182  mgcf1o  33236  gsumfs2d  33294  gsumhashmul  33300  gsummulsubdishift1  33301  cycpmco2lem5  33363  cycpmco2lem6  33364  cycpmco2lem7  33365  cycpmco2  33366  cyc3co2  33373  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnsubrunlem1  33480  erler  33498  fracerl  33542  imaslmod  33588  elrspunidl  33652  ressply1evls1  33772  ply1coedeg  33796  esplyfval3  33879  exsslsb  33904  dimpropd  33916  lbsdiflsp0  33933  extdg1id  33973  madjusmdetlem2  34135  zarcmplem  34188  eulerpartlemgvv  34683  boolesineq  34762  fineqvnttrclselem1  35429  vonf1wev  35463  vonf1owevOLD  35465  pfxwlk  35487  revwlk  35488  pthhashvtx  35491  spthcycl  35492  umgracycusgr  35517  subfacp1lem5  35547  satfvsucsuc  35728  ply1divalg3  36005  weiunfrlem  36837  ttctr  36866  dfttc2g  36879  cnambfre  38179  mapdordlem2  42273  frlmvscadiccat  43140  ricdrng1  43158  evlsbagval  43180  0prjspn  43222  3cubes  43283  oninfint  43825  onexomgt  43830  onexoegt  43833  ordeldif  43847  oacl2g  43919  onmcl  43920  omabs2  43921  omcl2  43922  tfsconcatfv  43930  tfsconcatrev  43937  ofoafg  43943  ofoafo  43945  ofoaass  43949  ofoacom  43950  onsucunifi  43959  oaun3lem1  43963  oadif1lem  43968  oadif1  43969  naddwordnexlem4  43990  safesnsupfilb  44006  gneispace  44722  rr-phpd  44797  grumnudlem  44859  ax6e2ndeqALT  45504  sineq0ALT  45510  fnresdmss  45744  saliinclf  46898  hoicvr  47120  setsv  47982  sprsymrelfolem2  48097  lighneal  48218  indprmfz  48237  grimuhgr  48507  grimcnv  48508  uhgrimedgi  48510  uhgrimedg  48511  isuspgrim0lem  48513  isuspgrim0  48514  upgrimtrlslem1  48524  upgrimtrlslem2  48525  clnbgrgrim  48554  grimedg  48555  isubgr3stgrlem8  48593  clnbgr3stgrgrlim  48639  clnbgr3stgrgrlic  48640  lincresunit3  49112  2itscp  49412  resccat  49703