Theorem syl2an2r 698

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5104  axprlem4OLD  5399  brcogw  5852  funfni  6642  f1un  6842  fvelimab  6954  dff3  7097  fnex  7220  ralima  7240  f1cofveqaeq  7258  f1eqcocnv  7306  caofid0l  7715  caofid0r  7716  caofid1  7717  caofid2  7718  onmindif2  7810  limsssuc  7850  mptcnfimad  7987  fnse  8135  frrlem13  8301  iinon  8333  smoord  8358  smoword  8359  tfrlem11  8381  coflton  8663  cofonr  8666  naddasslem2  8688  boxcutc  8952  f1domg  8981  phpeqd  9210  ominf  9238  f1finf1o  9247  unfilem1  9279  f1opwfi  9327  marypha2  9413  supmax  9442  infmin  9470  ordtypelem6  9499  oiexg  9511  oien  9514  cantnff  9657  cantnfp1lem3  9663  cantnflem1b  9669  cantnflem1  9672  ttrcltr  9699  ttrclselem2  9709  opwf  9798  rankopb  9838  xpnum  9960  infxpenlem  10020  infxp  10220  cflim2  10269  cofsmo  10275  cfsmolem  10276  cfcoflem  10278  ssfin3ds  10336  isf34lem5  10384  isf34lem6  10386  isfin1-3  10392  axcc3  10444  alephval2  10585  fpwwe2lem7  10650  canthp1  10667  tsken  10767  ltaddpr  11047  dedekind  11401  recextlem2  11873  recex  11874  gt0div  12109  ge0div  12110  lerec2  12131  uzwo2  12965  infssuzcl  12985  qmulcl  13021  xnegdi  13304  xmulpnf1n  13334  xadddi2  13353  fzm1  13666  2submod  14000  addmodlteq  14014  expnlbnd  14301  faclbnd5  14366  hasheni  14416  hashdifpr  14484  hashgt23el  14493  ccatrn  14659  ccatf1  14660  ccatalpha  14664  swrds1  14740  swrdccat2  14743  ccatpfx  14774  swrdccatin2  14802  pfxccatin12lem2  14804  revccat  14839  revrev  14840  swrdco  14912  relexpindlem  15140  resqrex  15341  fzomaxdiflem  15434  climconst  15634  serf0  15772  fsumf1o  15813  fsumrev  15869  fsumabs  15892  cvgcmp  15907  binomlem  15922  isumshft  15932  climcndslem1  15942  climcndslem2  15943  climcnds  15944  supcvg  15949  fprodcl2lem  16043  tanneg  16242  rpnnen2lem11  16318  modm1div  16360  fzo0dvdseq  16419  bitsfzolem  16530  gcdcllem3  16597  hashdvds  16872  prmdivdiv  16884  reumodprminv  16902  nnnn0modprm0  16904  pythagtrip  16932  dvdsprmpweqle  16984  pockthg  17004  4sqlem9  17044  vdwmc2  17077  vdwlem2  17080  imasaddflem  17622  acsfn1  17755  acsfn1c  17756  acsfn2  17757  oppccofval  17810  rescabs  17928  diag2  18339  grpinvalem  18773  issubmnd  18872  imasmnd  18888  pwsco2mhm  18948  gsumwspan  18961  frmdss2  18978  grpinvssd  19146  pwssub  19183  imasgrp  19185  subginv  19262  subginvcl  19264  ecqusaddcl  19327  ghmpreima  19371  conjnsg  19387  gass  19434  gsmsymgreqlem2  19564  f1omvdmvd  19576  symgsssg  19600  symgfisg  19601  symgtrinv  19605  psgnunilem5  19627  sylow1lem2  19732  odcau  19737  sylow2a  19752  sylow2  19759  efgsp1  19870  frgpuptf  19903  frgpuptinv  19904  frgpupf  19906  frgpup3lem  19910  mulgdi  19959  gsumval3eu  20037  gsumzsplit  20060  gsumzmhm  20070  gsumxp2  20113  prdsgsum  20114  fsfnn0gsumfsffz  20116  ablfaclem3  20222  srgbinomlem  20375  gsummgp0  20464  pwsgprod  20476  imasring  20477  dvdsr01  20518  rngisom1  20613  01eq0ring  20697  issubrng2  20726  subrgcrng  20743  subrginv  20756  isdrngd  20937  imadrhmcl  20969  abv1z  20996  lcomfsupp  21092  lmodvneg1  21095  lspsn  21192  lmhmco  21233  lmhmima  21237  lmhmpreima  21238  reslmhm  21242  lbsextlem2  21352  isridlrng  21413  lidl0cl  21414  lidlunin0  21430  rspvalint  21438  elrspsn  21440  rnglidlmmgm  21448  rnglidlmsgrp  21449  2idlcpblrng  21479  quscrng  21492  rngqiprngghmlem1  21496  rngqiprngghmlem3  21498  rngqiprnglinlem3  21502  rngqiprngimf1lem  21503  rngqiprngimf  21506  rng2idl1cntr  21514  qsidomlem1  21549  qsidomlem2  21550  ssdifidllem  21553  ssdifidlprm  21555  znfld  21779  ipassr2  21866  ocvin  21893  pjfo  21934  obsne0  21944  frlmgsum  21991  aspval2  22119  psrlinv  22176  mplsubglem  22219  mpllsslem  22220  evlslem4  22298  evlslem1  22304  evlsval3  22311  mpfind  22337  evls1rhm  22553  madetsumid  22689  scmatcrng  22749  mdetleib2  22816  cramerimplem1  22914  m2pmfzgsumcl  22979  decpmatmul  23003  pmatcollpwscmat  23022  idpm2idmp  23032  pm2mpmhmlem1  23049  chpscmatgsummon  23076  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  topbas  23203  uncld  23272  incld  23274  elcls  23304  neiptopnei  23363  resttopon  23392  restdis  23409  cnclima  23499  paste  23525  cncmp  23623  clsconn  23661  conncompcld  23665  1stcfb  23676  2ndcsb  23680  2ndcredom  23681  kgencmp2  23778  txss12  23837  qtoptop2  23931  qtoptopon  23936  hmphindis  24029  uffixfr  24155  ufildr  24163  isfcls2  24245  tgplacthmeo  24335  tsmsgsum  24371  tgptsmscld  24383  tsmssplit  24384  ustuqtop5  24477  uspreg  24505  prdsxmetlem  24600  prdsbl  24723  metss  24740  metrest  24756  nrmmetd  24806  isngp2  24829  ngpsubcan  24846  lssnlm  24933  nmoid  24974  opnreen  25064  mpomulcn  25101  evth  25193  htpyco2  25213  phtpyco2  25224  clmvz  25345  tcphcph  25471  iscmet3  25527  metcld  25540  bcthlem2  25559  cssbn  25609  chlcsschl  25612  minveclem1  25658  evthicc2  25694  ovolunlem1a  25730  ovolicc2lem1  25751  ovolicc2lem4  25754  ovolicc2lem5  25755  uniioombllem2  25817  uniioombllem3  25819  vitalilem2  25843  vitalilem4  25845  vitalilem5  25846  itg2monolem1  25984  cpnres  26171  rolle  26224  dvlip2  26229  dvivthlem2  26243  dvfsumrlimge0  26264  deg1pwle  26352  plydivlem4  26533  ulm0  26634  efif1olem1  26787  efif1olem2  26788  eflogeq  26847  argimlt0  26858  logrec  27008  relogbcxp  27030  atanlogadd  27159  atanlogsub  27161  atantan  27168  ftalem4  27320  ftalem5  27321  basellem3  27327  chtub  27456  dchrpt  27511  dchrsum2  27512  gausslemma2dlem1a  27609  2lgslem3a1  27644  2lgslem3b1  27645  2lgslem3c1  27646  2lgslem3d1  27647  2lgsoddprm  27660  dchrisumlem2  27734  pntrsumbnd2  27811  nosupbnd1lem4  27955  noinfbnd2lem1  27974  cutbdaylt  28071  oldlim  28160  madebday  28173  cofcutr  28197  addbday  28291  negbdaylem  28329  absmuls  28517  absnegs  28520  bdayfinlem  28759  cnvmot  28891  tglineneq  29000  midexlem  29051  midex  29100  plngrotlem1  29152  axlowdimlem14  29420  uhgrspansubgrlem  29758  usgrres  29776  usgrnbcnvfv  29833  finsumvtxdg2sstep  30017  uspgr2wlkeq  30113  redwlk  30138  pfxwlk  30153  revwlk  30154  pthdivtx  30199  pthhashvtx  30202  usgr2wlkspthlem2  30231  spthcycl  30279  wwlknvtx  30321  2wlkdlem6  30407  umgr2wlkon  30426  rusgrnumwwlk  30454  clwwlkwwlksb  30532  clwwlknwwlksnb  30533  clwwnisshclwwsn  30537  clwwlknscsh  30540  clwlknf1oclwwlknlem1  30559  1wlkdlem2  30616  fusgreghash2wsp  30826  2clwwlklem  30831  2clwwlk2clwwlk  30838  numclwwlk6  30878  prssad  33012  prssbd  33013  ofrn2  33121  ofpreima2  33147  sgnval2  33214  argcj  33227  wrdsplex  33390  mgcf1o  33451  gsumfs2d  33509  gsumhashmul  33515  gsummulsubdishift1  33516  cycpmco2lem5  33578  cycpmco2lem6  33579  cycpmco2lem7  33580  cycpmco2  33581  cyc3co2  33588  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnsubrunlem1  33695  erler  33713  fracerl  33755  imaslmod  33801  elrspunidl  33864  ressply1evls1  33983  ply1coedeg  34007  esplyfval3  34090  exsslsb  34115  dimpropd  34127  lbsdiflsp0  34144  extdg1id  34184  madjusmdetlem2  34346  zarcmplem  34399  eulerpartlemgvv  34895  boolesineq  34974  fineqvnttrclselem1  35655  vonf1wev  35713  vonf1owevOLD  35715  umgracycusgr  35741  subfacp1lem5  35771  satfvsucsuc  35952  ply1divalg3  36229  weiunfrlem  37091  ttctr  37120  dfttc2g  37133  cnambfre  38425  mapdordlem2  42518  frlmvscadiccat  43402  ricdrng1  43418  evlsbagval  43440  0prjspn  43482  3cubes  43543  oninfint  44085  onexomgt  44090  onexoegt  44093  ordeldif  44107  oacl2g  44179  onmcl  44180  omabs2  44181  omcl2  44182  tfsconcatfv  44190  tfsconcatrev  44197  ofoafg  44203  ofoafo  44205  ofoaass  44209  ofoacom  44210  onsucunifi  44219  oaun3lem1  44223  oadif1lem  44228  oadif1  44229  naddwordnexlem4  44250  safesnsupfilb  44266  gneispace  44982  rr-phpd  45055  grumnudlem  45117  ax6e2ndeqALT  45761  sineq0ALT  45767  hashnnlt  45853  fnresdmss  46008  saliinclf  47162  hoicvr  47384  tmachlem-agreeprod  47773  setsv  48286  sprsymrelfolem2  48401  lighneal  48522  indprmfz  48541  grimuhgr  48811  grimcnv  48812  uhgrimedgi  48814  uhgrimedg  48815  isuspgrim0lem  48817  isuspgrim0  48818  upgrimtrlslem1  48828  upgrimtrlslem2  48829  clnbgrgrim  48858  grimedg  48859  isubgr3stgrlem8  48897  clnbgr3stgrgrlim  48943  clnbgr3stgrgrlic  48944  lincresunit3  49419  2itscp  49719  resccat  50008