Theorem syl2an2r 683

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 397

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 206  df-an 398

This theorem is referenced by:  disjxiun  5078  axprlem4  5358  brcogw  5790  funfni  6570  f1un  6766  fvelimab  6873  dff3  7008  fnex  7125  f1cofveqaeq  7163  f1eqcocnv  7205  f1eqcocnvOLD  7206  caofid0l  7596  caofid0r  7597  caofid1  7598  caofid2  7599  onmindif2  7689  limsssuc  7729  fnse  8005  frrlem13  8145  iinon  8202  smoord  8227  smoword  8228  tfrlem11  8250  boxcutc  8760  f1domg  8793  phpeqd  9036  phpeqdOLD  9046  findcard3  9101  unfilem1  9122  f1opwfi  9167  marypha2  9242  supmax  9270  infmin  9297  ordtypelem6  9326  oiexg  9338  oien  9341  cantnff  9476  cantnfp1lem3  9482  cantnflem1b  9488  cantnflem1  9491  ttrcltr  9518  ttrclselem2  9528  opwf  9614  rankopb  9654  xpnum  9753  infxpenlem  9815  infxp  10017  cflim2  10065  cofsmo  10071  cfsmolem  10072  cfcoflem  10074  ssfin3ds  10132  isf34lem5  10180  isf34lem6  10182  isfin1-3  10188  axcc3  10240  alephval2  10374  fpwwe2lem7  10439  canthp1  10456  tsken  10556  ltaddpr  10836  dedekind  11184  recextlem2  11652  recex  11653  gt0div  11887  ge0div  11888  lerec2  11909  uzwo2  12698  infssuzcl  12718  qmulcl  12753  xnegdi  13028  xmulpnf1n  13058  xadddi2  13077  fzm1  13382  2submod  13698  addmodlteq  13712  expnlbnd  13994  faclbnd5  14058  hasheni  14108  hashdifpr  14175  hashgt23el  14184  ccatrn  14339  ccatalpha  14343  swrds1  14424  swrdccat2  14427  ccatpfx  14459  swrdccatin2  14487  pfxccatin12lem2  14489  revccat  14524  revrev  14525  swrdco  14595  relexpindlem  14819  resqrex  15007  fzomaxdiflem  15099  climconst  15297  serf0  15437  fsumf1o  15480  fsumrev  15536  fsumabs  15558  cvgcmp  15573  binomlem  15586  isumshft  15596  climcndslem1  15606  climcndslem2  15607  climcnds  15608  supcvg  15613  fprodcl2lem  15705  tanneg  15902  rpnnen2lem11  15978  modm1div  16020  fzo0dvdseq  16077  bitsfzolem  16186  gcdcllem3  16253  hashdvds  16521  prmdivdiv  16533  reumodprminv  16550  nnnn0modprm0  16552  pythagtrip  16580  dvdsprmpweqle  16632  pockthg  16652  4sqlem9  16692  vdwmc2  16725  vdwlem2  16728  imasaddflem  17286  acsfn1  17415  acsfn1c  17416  acsfn2  17417  oppccofval  17471  rescabs  17592  diag2  18008  grprinvlem  18402  issubmnd  18457  imasmnd  18468  pwsco2mhm  18516  gsumwspan  18530  frmdss2  18547  grpinvssd  18697  pwssub  18734  imasgrp  18736  subginv  18807  subginvcl  18809  ghmpreima  18901  conjnsg  18915  gass  18952  gsmsymgreqlem2  19084  f1omvdmvd  19096  symgsssg  19120  symgfisg  19121  symgtrinv  19125  psgnunilem5  19147  sylow1lem2  19249  odcau  19254  sylow2a  19269  sylow2  19276  efgsp1  19388  frgpuptf  19421  frgpuptinv  19422  frgpupf  19424  frgpup3lem  19428  mulgdi  19473  gsumval3eu  19550  gsumzsplit  19573  gsumzmhm  19583  gsumxp2  19626  prdsgsum  19627  fsfnn0gsumfsffz  19629  ablfaclem3  19735  srgbinomlem  19825  gsummgp0  19892  imasring  19903  dvdsr01  19942  subrgcrng  20073  subrginv  20085  abv1z  20137  lcomfsupp  20208  lmodvneg1  20211  lspsn  20309  lmhmco  20350  lmhmima  20354  lmhmpreima  20355  reslmhm  20359  lbsextlem2  20466  lidl0cl  20528  znfld  20813  ipassr2  20897  ocvin  20924  pjfo  20967  obsne0  20977  frlmgsum  21024  aspval2  21147  psrlinv  21211  mplsubglem  21250  mpllsslem  21251  evlslem4  21329  evlslem1  21337  mpfind  21362  evls1rhm  21533  madetsumid  21655  scmatcrng  21715  mdetleib2  21782  cramerimplem1  21877  m2pmfzgsumcl  21942  decpmatmul  21966  pmatcollpwscmat  21985  idpm2idmp  21995  pm2mpmhmlem1  22012  chpscmatgsummon  22039  chfacfscmulgsum  22054  chfacfpmmulgsum  22058  topbas  22167  uncld  22237  incld  22239  elcls  22269  neiptopnei  22328  resttopon  22357  restdis  22374  cnclima  22464  paste  22490  cncmp  22588  clsconn  22626  conncompcld  22630  1stcfb  22641  2ndcsb  22645  2ndcredom  22646  kgencmp2  22742  txss12  22801  qtoptop2  22895  qtoptopon  22900  hmphindis  22993  uffixfr  23119  ufildr  23127  isfcls2  23209  tgplacthmeo  23299  tsmsgsum  23335  tgptsmscld  23347  tsmssplit  23348  ustuqtop5  23442  uspreg  23471  prdsxmetlem  23566  prdsbl  23692  metss  23709  metrest  23725  nrmmetd  23775  isngp2  23798  ngpsubcan  23815  lssnlm  23910  nmoid  23951  opnreen  24039  evth  24167  htpyco2  24187  phtpyco2  24198  clmvz  24319  tcphcph  24446  iscmet3  24502  metcld  24515  bcthlem2  24534  cssbn  24584  chlcsschl  24587  minveclem1  24633  evthicc2  24669  ovolunlem1a  24705  ovolicc2lem1  24726  ovolicc2lem4  24729  ovolicc2lem5  24730  uniioombllem2  24792  uniioombllem3  24794  vitalilem2  24818  vitalilem4  24820  vitalilem5  24821  itg2monolem1  24960  cpnres  25146  rolle  25199  dvlip2  25204  dvivthlem2  25218  dvfsumrlimge0  25239  deg1pwle  25329  plydivlem4  25501  ulm0  25595  efif1olem1  25743  efif1olem2  25744  eflogeq  25802  argimlt0  25813  logrec  25958  relogbcxp  25980  atanlogadd  26109  atanlogsub  26111  atantan  26118  ftalem4  26270  ftalem5  26271  basellem3  26277  chtub  26405  dchrpt  26460  dchrsum2  26461  gausslemma2dlem1a  26558  2lgslem3a1  26593  2lgslem3b1  26594  2lgslem3c1  26595  2lgslem3d1  26596  2lgsoddprm  26609  dchrisumlem2  26683  pntrsumbnd2  26760  cnvmot  26947  tglineneq  27050  midexlem  27098  midex  27143  axlowdimlem14  27368  uhgrspansubgrlem  27702  usgrres  27720  usgrnbcnvfv  27777  finsumvtxdg2sstep  27961  uspgr2wlkeq  28058  redwlk  28085  pthdivtx  28142  usgr2wlkspthlem2  28171  wwlknvtx  28255  2wlkdlem6  28341  umgr2wlkon  28360  rusgrnumwwlk  28385  clwwlkwwlksb  28463  clwwlknwwlksnb  28464  clwwnisshclwwsn  28468  clwwlknscsh  28471  clwlknf1oclwwlknlem1  28490  1wlkdlem2  28547  fusgreghash2wsp  28747  2clwwlklem  28752  2clwwlk2clwwlk  28759  numclwwlk6  28799  ofrn2  31022  ofpreima2  31048  wrdsplex  31257  ccatf1  31268  mgcf1o  31326  gsumhashmul  31361  cycpmco2lem5  31442  cycpmco2lem6  31443  cycpmco2lem7  31444  cycpmco2  31445  cyc3co2  31452  imaslmod  31598  rspsnel  31612  elrspunidl  31651  qsidomlem1  31673  qsidomlem2  31674  dimpropd  31737  lbsdiflsp0  31752  extdg1id  31783  zarcmplem  31876  eulerpartlemgvv  32388  pfxwlk  33130  revwlk  33131  pthhashvtx  33134  spthcycl  33136  umgracycusgr  33161  subfacp1lem5  33191  satfvsucsuc  33372  nosupbnd1lem4  33959  noinfbnd2lem1  33978  scutbdaylt  34057  oldlim  34114  madebday  34125  cofcutr  34137  cnambfre  35869  frlmvscadiccat  40274  pwsgprod  40306  evlsval3  40309  evlsbagval  40312  0prjspn  40502  3cubes  40549  gneispace  41782  rr-phpd  41859  grumnudlem  41941  ax6e2ndeqALT  42589  sineq0ALT  42595  fnresdmss  42748  setsv  44888  sprsymrelfolem2  45003  lighneal  45121  isomuspgrlem2c  45340  lincresunit3  45880  2itscp  46185