Theorem syl2an2r 695

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  disjxiun  5096  axprlem4OLD  5386  brcogw  5838  funfni  6623  f1un  6823  fvelimab  6935  dff3  7077  fnex  7197  ralima  7217  f1cofveqaeq  7237  f1eqcocnv  7281  caofid0l  7689  caofid0r  7690  caofid1  7691  caofid2  7692  onmindif2  7786  limsssuc  7826  mptcnfimad  7963  fnse  8108  frrlem13  8274  iinon  8306  smoord  8331  smoword  8332  tfrlem11  8354  coflton  8636  cofonr  8639  naddasslem2  8661  boxcutc  8919  f1domg  8948  phpeqd  9176  ominf  9204  f1finf1o  9213  unfilem1  9245  f1opwfi  9296  marypha2  9382  supmax  9411  infmin  9439  ordtypelem6  9468  oiexg  9480  oien  9483  cantnff  9626  cantnfp1lem3  9632  cantnflem1b  9638  cantnflem1  9641  ttrcltr  9668  ttrclselem2  9678  opwf  9767  rankopb  9807  xpnum  9906  infxpenlem  9966  infxp  10167  cflim2  10217  cofsmo  10223  cfsmolem  10224  cfcoflem  10226  ssfin3ds  10284  isf34lem5  10332  isf34lem6  10334  isfin1-3  10340  axcc3  10392  alephval2  10527  fpwwe2lem7  10592  canthp1  10609  tsken  10709  ltaddpr  10989  dedekind  11343  recextlem2  11815  recex  11816  gt0div  12055  ge0div  12056  lerec2  12077  uzwo2  12910  infssuzcl  12930  qmulcl  12965  xnegdi  13248  xmulpnf1n  13278  xadddi2  13297  fzm1  13609  2submod  13942  addmodlteq  13956  expnlbnd  14243  faclbnd5  14308  hasheni  14358  hashdifpr  14425  hashgt23el  14434  ccatrn  14600  ccatalpha  14604  swrds1  14677  swrdccat2  14680  ccatpfx  14711  swrdccatin2  14739  pfxccatin12lem2  14741  revccat  14776  revrev  14777  swrdco  14847  relexpindlem  15073  resqrex  15260  fzomaxdiflem  15353  climconst  15553  serf0  15691  fsumf1o  15733  fsumrev  15789  fsumabs  15812  cvgcmp  15827  binomlem  15842  isumshft  15852  climcndslem1  15862  climcndslem2  15863  climcnds  15864  supcvg  15869  fprodcl2lem  15963  tanneg  16163  rpnnen2lem11  16239  modm1div  16281  fzo0dvdseq  16340  bitsfzolem  16451  gcdcllem3  16518  hashdvds  16793  prmdivdiv  16805  reumodprminv  16823  nnnn0modprm0  16825  pythagtrip  16853  dvdsprmpweqle  16905  pockthg  16925  4sqlem9  16965  vdwmc2  16998  vdwlem2  17001  imasaddflem  17543  acsfn1  17676  acsfn1c  17677  acsfn2  17678  oppccofval  17731  rescabs  17849  diag2  18260  grpinvalem  18690  issubmnd  18778  imasmnd  18792  pwsco2mhm  18850  gsumwspan  18863  frmdss2  18880  grpinvssd  19042  pwssub  19079  imasgrp  19081  subginv  19158  subginvcl  19160  ecqusaddcl  19217  ghmpreima  19261  conjnsg  19277  gass  19324  gsmsymgreqlem2  19454  f1omvdmvd  19466  symgsssg  19490  symgfisg  19491  symgtrinv  19495  psgnunilem5  19517  sylow1lem2  19622  odcau  19627  sylow2a  19642  sylow2  19649  efgsp1  19760  frgpuptf  19793  frgpuptinv  19794  frgpupf  19796  frgpup3lem  19800  mulgdi  19849  gsumval3eu  19927  gsumzsplit  19950  gsumzmhm  19960  gsumxp2  20003  prdsgsum  20004  fsfnn0gsumfsffz  20006  ablfaclem3  20112  srgbinomlem  20259  gsummgp0  20345  pwsgprod  20357  imasring  20358  dvdsr01  20399  rngisom1  20494  01eq0ring  20559  issubrng2  20587  subrgcrng  20604  subrginv  20617  isdrngd  20794  imadrhmcl  20826  abv1z  20853  lcomfsupp  20949  lmodvneg1  20952  lspsn  21049  lmhmco  21090  lmhmima  21094  lmhmpreima  21095  reslmhm  21099  lbsextlem2  21209  isridlrng  21269  lidl0cl  21270  elrspsn  21290  rnglidlmmgm  21295  rnglidlmsgrp  21296  2idlcpblrng  21321  quscrng  21333  rngqiprngghmlem1  21337  rngqiprngghmlem3  21339  rngqiprnglinlem3  21343  rngqiprngimf1lem  21344  rngqiprngimf  21347  rng2idl1cntr  21355  znfld  21592  ipassr2  21679  ocvin  21706  pjfo  21747  obsne0  21757  frlmgsum  21804  aspval2  21930  psrlinv  21987  mplsubglem  22030  mpllsslem  22031  evlslem4  22109  evlslem1  22115  evlsval3  22122  mpfind  22148  evls1rhm  22365  madetsumid  22501  scmatcrng  22561  mdetleib2  22628  cramerimplem1  22723  m2pmfzgsumcl  22788  decpmatmul  22812  pmatcollpwscmat  22831  idpm2idmp  22841  pm2mpmhmlem1  22858  chpscmatgsummon  22885  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  topbas  23012  uncld  23081  incld  23083  elcls  23113  neiptopnei  23172  resttopon  23201  restdis  23218  cnclima  23308  paste  23334  cncmp  23432  clsconn  23470  conncompcld  23474  1stcfb  23485  2ndcsb  23489  2ndcredom  23490  kgencmp2  23586  txss12  23645  qtoptop2  23739  qtoptopon  23744  hmphindis  23837  uffixfr  23963  ufildr  23971  isfcls2  24053  tgplacthmeo  24143  tsmsgsum  24179  tgptsmscld  24191  tsmssplit  24192  ustuqtop5  24285  uspreg  24313  prdsxmetlem  24408  prdsbl  24531  metss  24548  metrest  24564  nrmmetd  24614  isngp2  24637  ngpsubcan  24654  lssnlm  24741  nmoid  24782  opnreen  24872  mpomulcn  24909  evth  25001  htpyco2  25021  phtpyco2  25032  clmvz  25153  tcphcph  25279  iscmet3  25335  metcld  25348  bcthlem2  25367  cssbn  25417  chlcsschl  25420  minveclem1  25466  evthicc2  25502  ovolunlem1a  25538  ovolicc2lem1  25559  ovolicc2lem4  25562  ovolicc2lem5  25563  uniioombllem2  25625  uniioombllem3  25627  vitalilem2  25651  vitalilem4  25653  vitalilem5  25654  itg2monolem1  25792  cpnres  25979  rolle  26032  dvlip2  26037  dvivthlem2  26051  dvfsumrlimge0  26072  deg1pwle  26160  plydivlem4  26337  ulm0  26431  efif1olem1  26584  efif1olem2  26585  eflogeq  26644  argimlt0  26655  logrec  26805  relogbcxp  26827  atanlogadd  26956  atanlogsub  26958  atantan  26965  ftalem4  27117  ftalem5  27118  basellem3  27124  chtub  27253  dchrpt  27308  dchrsum2  27309  gausslemma2dlem1a  27406  2lgslem3a1  27441  2lgslem3b1  27442  2lgslem3c1  27443  2lgslem3d1  27444  2lgsoddprm  27457  dchrisumlem2  27531  pntrsumbnd2  27608  nosupbnd1lem4  27752  noinfbnd2lem1  27771  cutbdaylt  27868  oldlim  27957  madebday  27970  cofcutr  27994  addbday  28088  negbdaylem  28126  absmuls  28314  absnegs  28317  bdayfinlem  28556  cnvmot  28687  tglineneq  28790  midexlem  28838  midex  28883  axlowdimlem14  29102  uhgrspansubgrlem  29437  usgrres  29455  usgrnbcnvfv  29512  finsumvtxdg2sstep  29696  uspgr2wlkeq  29792  redwlk  29817  pthdivtx  29873  usgr2wlkspthlem2  29904  wwlknvtx  29991  2wlkdlem6  30077  umgr2wlkon  30096  rusgrnumwwlk  30124  clwwlkwwlksb  30202  clwwlknwwlksnb  30203  clwwnisshclwwsn  30207  clwwlknscsh  30210  clwlknf1oclwwlknlem1  30229  1wlkdlem2  30286  fusgreghash2wsp  30486  2clwwlklem  30491  2clwwlk2clwwlk  30498  numclwwlk6  30538  prssad  32677  prssbd  32678  ofrn2  32792  ofpreima2  32818  sgnval2  32887  argcj  32900  wrdsplex  33075  ccatf1  33088  mgcf1o  33142  gsumfs2d  33202  gsumhashmul  33208  gsummulsubdishift1  33209  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmco2  33274  cyc3co2  33281  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnsubrunlem1  33389  erler  33407  fracerl  33454  imaslmod  33500  elrspunidl  33575  qsidomlem1  33600  qsidomlem2  33601  ssdifidllem  33604  ssdifidlprm  33606  ressply1evls1  33722  ply1coedeg  33746  esplyfval3  33830  exsslsb  33855  dimpropd  33867  lbsdiflsp0  33884  extdg1id  33924  madjusmdetlem2  34086  zarcmplem  34139  eulerpartlemgvv  34634  boolesineq  34713  fineqvnttrclselem1  35381  vonf1wev  35415  vonf1owevOLD  35417  pfxwlk  35438  revwlk  35439  pthhashvtx  35442  spthcycl  35443  umgracycusgr  35468  subfacp1lem5  35498  satfvsucsuc  35679  ply1divalg3  35956  weiunfrlem  36788  ttctr  36817  dfttc2g  36830  cnambfre  38131  mapdordlem2  42225  frlmvscadiccat  43092  ricdrng1  43110  evlsbagval  43132  0prjspn  43174  3cubes  43235  oninfint  43777  onexomgt  43782  onexoegt  43785  ordeldif  43799  oacl2g  43871  onmcl  43872  omabs2  43873  omcl2  43874  tfsconcatfv  43882  tfsconcatrev  43889  ofoafg  43895  ofoafo  43897  ofoaass  43901  ofoacom  43902  onsucunifi  43911  oaun3lem1  43915  oadif1lem  43920  oadif1  43921  naddwordnexlem4  43942  safesnsupfilb  43958  gneispace  44674  rr-phpd  44749  grumnudlem  44825  ax6e2ndeqALT  45470  sineq0ALT  45476  fnresdmss  45710  saliinclf  46864  hoicvr  47086  setsv  47948  sprsymrelfolem2  48063  lighneal  48184  indprmfz  48203  grimuhgr  48473  grimcnv  48474  uhgrimedgi  48476  uhgrimedg  48477  isuspgrim0lem  48479  isuspgrim0  48480  upgrimtrlslem1  48490  upgrimtrlslem2  48491  clnbgrgrim  48520  grimedg  48521  isubgr3stgrlem8  48559  clnbgr3stgrgrlim  48605  clnbgr3stgrgrlic  48606  lincresunit3  49067  2itscp  49367  resccat  49659