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 582	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 593	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  disjxiun  5065  axprlem4  5329  brcogw  5741  funfni  6459  fvelimab  6739  dff3  6868  fnex  6982  f1cofveqaeq  7018  f1eqcocnv  7059  caofid0l  7439  caofid0r  7440  caofid1  7441  caofid2  7442  onmindif2  7529  limsssuc  7567  fnse  7829  iinon  7979  smoord  8004  smoword  8005  tfrlem11  8026  boxcutc  8507  f1domg  8531  phpeqd  8708  findcard3  8763  unfilem1  8784  f1opwfi  8830  marypha2  8905  supmax  8933  infmin  8960  ordtypelem6  8989  oiexg  9001  oien  9004  cantnff  9139  cantnfp1lem3  9145  cantnflem1b  9151  cantnflem1  9154  opwf  9243  rankopb  9283  xpnum  9382  infxpenlem  9441  infxp  9639  cflim2  9687  cofsmo  9693  cfsmolem  9694  cfcoflem  9696  ssfin3ds  9754  isf34lem5  9802  isf34lem6  9804  isfin1-3  9810  axcc3  9862  alephval2  9996  fpwwe2lem8  10061  canthp1  10078  tsken  10178  ltaddpr  10458  dedekind  10805  recextlem2  11273  recex  11274  gt0div  11508  ge0div  11509  lerec2  11530  uzwo2  12315  infssuzcl  12335  qmulcl  12369  xnegdi  12644  xmulpnf1n  12674  xadddi2  12693  fzm1  12990  2submod  13303  addmodlteq  13317  expnlbnd  13597  faclbnd5  13661  hasheni  13711  hashdifpr  13779  hashgt23el  13788  ccatrn  13945  ccatalpha  13949  swrds1  14030  swrdccat2  14033  ccatpfx  14065  swrdccatin2  14093  pfxccatin12lem2  14095  revccat  14130  revrev  14131  swrdco  14201  relexpindlem  14424  resqrex  14612  fzomaxdiflem  14704  climconst  14902  serf0  15039  fsumf1o  15082  fsumrev  15136  fsumabs  15158  cvgcmp  15173  binomlem  15186  isumshft  15196  climcndslem1  15206  climcndslem2  15207  climcnds  15208  supcvg  15213  fprodcl2lem  15306  tanneg  15503  rpnnen2lem11  15579  modm1div  15621  fzo0dvdseq  15675  bitsfzolem  15785  gcdcllem3  15852  hashdvds  16114  prmdivdiv  16126  reumodprminv  16143  nnnn0modprm0  16145  pythagtrip  16173  dvdsprmpweqle  16224  pockthg  16244  4sqlem9  16284  vdwmc2  16317  vdwlem2  16320  imasaddflem  16805  acsfn1  16934  acsfn1c  16935  acsfn2  16936  oppccofval  16988  diag2  17497  grprinvlem  17885  issubmnd  17940  imasmnd  17951  pwsco2mhm  17999  gsumwspan  18013  frmdss2  18030  grpinvssd  18178  pwssub  18215  imasgrp  18217  subginv  18288  subginvcl  18290  ghmpreima  18382  conjnsg  18396  gass  18433  gsmsymgreqlem2  18561  f1omvdmvd  18573  symgsssg  18597  symgfisg  18598  symgtrinv  18602  psgnunilem5  18624  sylow1lem2  18726  odcau  18731  sylow2  18753  efgsp1  18865  frgpuptf  18898  frgpuptinv  18899  frgpupf  18901  frgpup3lem  18905  mulgdi  18949  gsumval3eu  19026  gsumzsplit  19049  gsumzmhm  19059  gsumxp2  19102  prdsgsum  19103  fsfnn0gsumfsffz  19105  ablfaclem3  19211  srgbinomlem  19296  gsummgp0  19360  imasring  19371  dvdsr01  19407  subrgcrng  19541  subrginv  19553  abv1z  19605  lcomfsupp  19676  lmodvneg1  19679  lspsn  19776  lmhmco  19817  lmhmima  19821  lmhmpreima  19822  reslmhm  19826  lbsextlem2  19933  lidl0cl  19987  aspval2  20129  psrlinv  20179  mplsubglem  20216  mpllsslem  20217  evlslem4  20290  evlslem1  20297  mpfind  20322  evls1rhm  20487  znfld  20709  ipassr2  20793  ocvin  20820  pjfo  20861  obsne0  20871  frlmgsum  20918  madetsumid  21072  scmatcrng  21132  mdetleib2  21199  cramerimplem1  21294  m2pmfzgsumcl  21358  decpmatmul  21382  pmatcollpwscmat  21401  idpm2idmp  21411  pm2mpmhmlem1  21428  chpscmatgsummon  21455  chfacfscmulgsum  21470  chfacfpmmulgsum  21474  topbas  21582  uncld  21651  incld  21653  elcls  21683  neiptopnei  21742  resttopon  21771  restdis  21788  cnclima  21878  paste  21904  cncmp  22002  clsconn  22040  conncompcld  22044  1stcfb  22055  2ndcsb  22059  2ndcredom  22060  kgencmp2  22156  txss12  22215  qtoptop2  22309  qtoptopon  22314  hmphindis  22407  uffixfr  22533  ufildr  22541  isfcls2  22623  tgplacthmeo  22713  tsmsgsum  22749  tgptsmscld  22761  tsmssplit  22762  ustuqtop5  22856  uspreg  22885  prdsxmetlem  22980  prdsbl  23103  metss  23120  metrest  23136  nrmmetd  23186  isngp2  23208  ngpsubcan  23225  lssnlm  23312  nmoid  23353  opnreen  23441  evth  23565  htpyco2  23585  phtpyco2  23596  clmvz  23717  tcphcph  23842  iscmet3  23898  metcld  23911  bcthlem2  23930  cssbn  23980  chlcsschl  23983  minveclem1  24029  evthicc2  24063  ovolunlem1a  24099  ovolicc2lem1  24120  ovolicc2lem4  24123  ovolicc2lem5  24124  uniioombllem2  24186  uniioombllem3  24188  vitalilem2  24212  vitalilem4  24214  vitalilem5  24215  itg2monolem1  24353  cpnres  24536  rolle  24589  dvlip2  24594  dvivthlem2  24608  dvfsumrlimge0  24629  deg1pwle  24715  plydivlem4  24887  ulm0  24981  efif1olem1  25128  efif1olem2  25129  eflogeq  25187  argimlt0  25198  logrec  25343  relogbcxp  25365  atanlogadd  25494  atanlogsub  25496  atantan  25503  ftalem4  25655  ftalem5  25656  basellem3  25662  chtub  25790  dchrpt  25845  dchrsum2  25846  gausslemma2dlem1a  25943  2lgslem3a1  25978  2lgslem3b1  25979  2lgslem3c1  25980  2lgslem3d1  25981  2lgsoddprm  25994  dchrisumlem2  26068  pntrsumbnd2  26145  cnvmot  26329  tglineneq  26432  midexlem  26480  midex  26525  axlowdimlem14  26743  uhgrspansubgrlem  27074  usgrres  27092  usgrnbcnvfv  27149  finsumvtxdg2sstep  27333  uspgr2wlkeq  27429  redwlk  27456  pthdivtx  27512  usgr2wlkspthlem2  27541  wwlknvtx  27625  2wlkdlem6  27712  umgr2wlkon  27731  rusgrnumwwlk  27756  clwwlkwwlksb  27835  clwwlknwwlksnb  27836  clwwnisshclwwsn  27840  clwwlknscsh  27843  clwlknf1oclwwlknlem1  27862  1wlkdlem2  27919  fusgreghash2wsp  28119  2clwwlklem  28124  2clwwlk2clwwlk  28131  numclwwlk6  28171  ofrn2  30389  ofpreima2  30413  wrdsplex  30616  ccatf1  30627  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2lem7  30776  cycpmco2  30777  cyc3co2  30784  imaslmod  30924  rspsnel  30938  qsidomlem1  30967  qsidomlem2  30968  dimpropd  31009  lbsdiflsp0  31024  extdg1id  31055  eulerpartlemgvv  31636  pfxwlk  32372  revwlk  32373  pthhashvtx  32376  spthcycl  32378  umgracycusgr  32403  satfvsucsuc  32614  frrlem13  33137  nosupbnd1lem4  33213  scutbdaylt  33278  cnambfre  34942  frlmvscadiccat  39152  0prjspn  39277  3cubes  39294  gneispace  40491  rr-phpd  40569  grumnudlem  40628  ax6e2ndeqALT  41272  sineq0ALT  41278  fnresdmss  41431  setsv  43545  sprsymrelfolem2  43662  lighneal  43783  isomuspgrlem2c  44002  lincresunit3  44543  2itscp  44775