Theorem syl2an2r 684

Description: syl2anr 599 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 583	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 594	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 210  df-an 400

This theorem is referenced by:  disjxiun  5027  axprlem4  5292  brcogw  5703  funfni  6428  fvelimab  6712  dff3  6843  fnex  6957  f1cofveqaeq  6994  f1eqcocnv  7035  f1eqcocnvOLD  7036  caofid0l  7417  caofid0r  7418  caofid1  7419  caofid2  7420  onmindif2  7507  limsssuc  7545  fnse  7810  iinon  7960  smoord  7985  smoword  7986  tfrlem11  8007  boxcutc  8488  f1domg  8512  phpeqd  8690  findcard3  8745  unfilem1  8766  f1opwfi  8812  marypha2  8887  supmax  8915  infmin  8942  ordtypelem6  8971  oiexg  8983  oien  8986  cantnff  9121  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1  9136  opwf  9225  rankopb  9265  xpnum  9364  infxpenlem  9424  infxp  9626  cflim2  9674  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  ssfin3ds  9741  isf34lem5  9789  isf34lem6  9791  isfin1-3  9797  axcc3  9849  alephval2  9983  fpwwe2lem8  10048  canthp1  10065  tsken  10165  ltaddpr  10445  dedekind  10792  recextlem2  11260  recex  11261  gt0div  11495  ge0div  11496  lerec2  11517  uzwo2  12300  infssuzcl  12320  qmulcl  12354  xnegdi  12629  xmulpnf1n  12659  xadddi2  12678  fzm1  12982  2submod  13295  addmodlteq  13309  expnlbnd  13590  faclbnd5  13654  hasheni  13704  hashdifpr  13772  hashgt23el  13781  ccatrn  13934  ccatalpha  13938  swrds1  14019  swrdccat2  14022  ccatpfx  14054  swrdccatin2  14082  pfxccatin12lem2  14084  revccat  14119  revrev  14120  swrdco  14190  relexpindlem  14414  resqrex  14602  fzomaxdiflem  14694  climconst  14892  serf0  15029  fsumf1o  15072  fsumrev  15126  fsumabs  15148  cvgcmp  15163  binomlem  15176  isumshft  15186  climcndslem1  15196  climcndslem2  15197  climcnds  15198  supcvg  15203  fprodcl2lem  15296  tanneg  15493  rpnnen2lem11  15569  modm1div  15611  fzo0dvdseq  15665  bitsfzolem  15773  gcdcllem3  15840  hashdvds  16102  prmdivdiv  16114  reumodprminv  16131  nnnn0modprm0  16133  pythagtrip  16161  dvdsprmpweqle  16212  pockthg  16232  4sqlem9  16272  vdwmc2  16305  vdwlem2  16308  imasaddflem  16795  acsfn1  16924  acsfn1c  16925  acsfn2  16926  oppccofval  16978  diag2  17487  grprinvlem  17875  issubmnd  17930  imasmnd  17941  pwsco2mhm  17989  gsumwspan  18003  frmdss2  18020  grpinvssd  18168  pwssub  18205  imasgrp  18207  subginv  18278  subginvcl  18280  ghmpreima  18372  conjnsg  18386  gass  18423  gsmsymgreqlem2  18551  f1omvdmvd  18563  symgsssg  18587  symgfisg  18588  symgtrinv  18592  psgnunilem5  18614  sylow1lem2  18716  odcau  18721  sylow2  18743  efgsp1  18855  frgpuptf  18888  frgpuptinv  18889  frgpupf  18891  frgpup3lem  18895  mulgdi  18940  gsumval3eu  19017  gsumzsplit  19040  gsumzmhm  19050  gsumxp2  19093  prdsgsum  19094  fsfnn0gsumfsffz  19096  ablfaclem3  19202  srgbinomlem  19287  gsummgp0  19354  imasring  19365  dvdsr01  19401  subrgcrng  19532  subrginv  19544  abv1z  19596  lcomfsupp  19667  lmodvneg1  19670  lspsn  19767  lmhmco  19808  lmhmima  19812  lmhmpreima  19813  reslmhm  19817  lbsextlem2  19924  lidl0cl  19978  znfld  20252  ipassr2  20336  ocvin  20363  pjfo  20404  obsne0  20414  frlmgsum  20461  aspval2  20584  psrlinv  20635  mplsubglem  20672  mpllsslem  20673  evlslem4  20747  evlslem1  20754  mpfind  20779  evls1rhm  20946  madetsumid  21066  scmatcrng  21126  mdetleib2  21193  cramerimplem1  21288  m2pmfzgsumcl  21353  decpmatmul  21377  pmatcollpwscmat  21396  idpm2idmp  21406  pm2mpmhmlem1  21423  chpscmatgsummon  21450  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  topbas  21577  uncld  21646  incld  21648  elcls  21678  neiptopnei  21737  resttopon  21766  restdis  21783  cnclima  21873  paste  21899  cncmp  21997  clsconn  22035  conncompcld  22039  1stcfb  22050  2ndcsb  22054  2ndcredom  22055  kgencmp2  22151  txss12  22210  qtoptop2  22304  qtoptopon  22309  hmphindis  22402  uffixfr  22528  ufildr  22536  isfcls2  22618  tgplacthmeo  22708  tsmsgsum  22744  tgptsmscld  22756  tsmssplit  22757  ustuqtop5  22851  uspreg  22880  prdsxmetlem  22975  prdsbl  23098  metss  23115  metrest  23131  nrmmetd  23181  isngp2  23203  ngpsubcan  23220  lssnlm  23307  nmoid  23348  opnreen  23436  evth  23564  htpyco2  23584  phtpyco2  23595  clmvz  23716  tcphcph  23841  iscmet3  23897  metcld  23910  bcthlem2  23929  cssbn  23979  chlcsschl  23982  minveclem1  24028  evthicc2  24064  ovolunlem1a  24100  ovolicc2lem1  24121  ovolicc2lem4  24124  ovolicc2lem5  24125  uniioombllem2  24187  uniioombllem3  24189  vitalilem2  24213  vitalilem4  24215  vitalilem5  24216  itg2monolem1  24354  cpnres  24540  rolle  24593  dvlip2  24598  dvivthlem2  24612  dvfsumrlimge0  24633  deg1pwle  24720  plydivlem4  24892  ulm0  24986  efif1olem1  25134  efif1olem2  25135  eflogeq  25193  argimlt0  25204  logrec  25349  relogbcxp  25371  atanlogadd  25500  atanlogsub  25502  atantan  25509  ftalem4  25661  ftalem5  25662  basellem3  25668  chtub  25796  dchrpt  25851  dchrsum2  25852  gausslemma2dlem1a  25949  2lgslem3a1  25984  2lgslem3b1  25985  2lgslem3c1  25986  2lgslem3d1  25987  2lgsoddprm  26000  dchrisumlem2  26074  pntrsumbnd2  26151  cnvmot  26335  tglineneq  26438  midexlem  26486  midex  26531  axlowdimlem14  26749  uhgrspansubgrlem  27080  usgrres  27098  usgrnbcnvfv  27155  finsumvtxdg2sstep  27339  uspgr2wlkeq  27435  redwlk  27462  pthdivtx  27518  usgr2wlkspthlem2  27547  wwlknvtx  27631  2wlkdlem6  27717  umgr2wlkon  27736  rusgrnumwwlk  27761  clwwlkwwlksb  27839  clwwlknwwlksnb  27840  clwwnisshclwwsn  27844  clwwlknscsh  27847  clwlknf1oclwwlknlem1  27866  1wlkdlem2  27923  fusgreghash2wsp  28123  2clwwlklem  28128  2clwwlk2clwwlk  28135  numclwwlk6  28175  ofrn2  30401  ofpreima2  30429  wrdsplex  30640  ccatf1  30651  gsumhashmul  30741  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  cyc3co2  30832  imaslmod  30973  rspsnel  30987  elrspunidl  31014  qsidomlem1  31036  qsidomlem2  31037  dimpropd  31095  lbsdiflsp0  31110  extdg1id  31141  zarcmplem  31234  eulerpartlemgvv  31744  pfxwlk  32483  revwlk  32484  pthhashvtx  32487  spthcycl  32489  umgracycusgr  32514  satfvsucsuc  32725  frrlem13  33248  nosupbnd1lem4  33324  scutbdaylt  33389  cnambfre  35105  frlmvscadiccat  39440  0prjspn  39614  3cubes  39631  gneispace  40837  rr-phpd  40916  grumnudlem  40993  ax6e2ndeqALT  41637  sineq0ALT  41643  fnresdmss  41792  setsv  43895  sprsymrelfolem2  44010  lighneal  44129  isomuspgrlem2c  44348  lincresunit3  44890  2itscp  45195