Theorem syl2an2r 686

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 395

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 207  df-an 396

This theorem is referenced by:  disjxiun  5083  axprlem4OLD  5367  brcogw  5817  funfni  6598  f1un  6794  fvelimab  6906  dff3  7046  fnex  7165  ralima  7185  f1cofveqaeq  7205  f1eqcocnv  7249  caofid0l  7657  caofid0r  7658  caofid1  7659  caofid2  7660  onmindif2  7754  limsssuc  7794  mptcnfimad  7932  fnse  8076  frrlem13  8241  iinon  8273  smoord  8298  smoword  8299  tfrlem11  8320  coflton  8600  cofonr  8603  naddasslem2  8624  boxcutc  8882  f1domg  8911  phpeqd  9139  ominf  9167  f1finf1o  9176  unfilem1  9208  f1opwfi  9259  marypha2  9345  supmax  9374  infmin  9402  ordtypelem6  9431  oiexg  9443  oien  9446  cantnff  9586  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1  9601  ttrcltr  9628  ttrclselem2  9638  opwf  9727  rankopb  9767  xpnum  9866  infxpenlem  9926  infxp  10127  cflim2  10176  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  ssfin3ds  10243  isf34lem5  10291  isf34lem6  10293  isfin1-3  10299  axcc3  10351  alephval2  10486  fpwwe2lem7  10551  canthp1  10568  tsken  10668  ltaddpr  10948  dedekind  11300  recextlem2  11772  recex  11773  gt0div  12013  ge0div  12014  lerec2  12035  uzwo2  12853  infssuzcl  12873  qmulcl  12908  xnegdi  13191  xmulpnf1n  13221  xadddi2  13240  fzm1  13552  2submod  13885  addmodlteq  13899  expnlbnd  14186  faclbnd5  14251  hasheni  14301  hashdifpr  14368  hashgt23el  14377  ccatrn  14543  ccatalpha  14547  swrds1  14620  swrdccat2  14623  ccatpfx  14654  swrdccatin2  14682  pfxccatin12lem2  14684  revccat  14719  revrev  14720  swrdco  14790  relexpindlem  15016  resqrex  15203  fzomaxdiflem  15296  climconst  15496  serf0  15634  fsumf1o  15676  fsumrev  15732  fsumabs  15755  cvgcmp  15770  binomlem  15785  isumshft  15795  climcndslem1  15805  climcndslem2  15806  climcnds  15807  supcvg  15812  fprodcl2lem  15906  tanneg  16106  rpnnen2lem11  16182  modm1div  16224  fzo0dvdseq  16283  bitsfzolem  16394  gcdcllem3  16461  hashdvds  16736  prmdivdiv  16748  reumodprminv  16766  nnnn0modprm0  16768  pythagtrip  16796  dvdsprmpweqle  16848  pockthg  16868  4sqlem9  16908  vdwmc2  16941  vdwlem2  16944  imasaddflem  17485  acsfn1  17618  acsfn1c  17619  acsfn2  17620  oppccofval  17673  rescabs  17791  diag2  18202  grpinvalem  18632  issubmnd  18720  imasmnd  18734  pwsco2mhm  18792  gsumwspan  18805  frmdss2  18822  grpinvssd  18984  pwssub  19021  imasgrp  19023  subginv  19100  subginvcl  19102  ecqusaddcl  19159  ghmpreima  19204  conjnsg  19220  gass  19267  gsmsymgreqlem2  19397  f1omvdmvd  19409  symgsssg  19433  symgfisg  19434  symgtrinv  19438  psgnunilem5  19460  sylow1lem2  19565  odcau  19570  sylow2a  19585  sylow2  19592  efgsp1  19703  frgpuptf  19736  frgpuptinv  19737  frgpupf  19739  frgpup3lem  19743  mulgdi  19792  gsumval3eu  19870  gsumzsplit  19893  gsumzmhm  19903  gsumxp2  19946  prdsgsum  19947  fsfnn0gsumfsffz  19949  ablfaclem3  20055  srgbinomlem  20202  gsummgp0  20288  pwsgprod  20300  imasring  20301  dvdsr01  20342  rngisom1  20437  01eq0ring  20498  issubrng2  20526  subrgcrng  20543  subrginv  20556  isdrngd  20733  imadrhmcl  20765  abv1z  20792  lcomfsupp  20888  lmodvneg1  20891  lspsn  20988  lmhmco  21030  lmhmima  21034  lmhmpreima  21035  reslmhm  21039  lbsextlem2  21149  isridlrng  21209  lidl0cl  21210  elrspsn  21230  rnglidlmmgm  21235  rnglidlmsgrp  21236  2idlcpblrng  21261  quscrng  21273  rngqiprngghmlem1  21277  rngqiprngghmlem3  21279  rngqiprnglinlem3  21283  rngqiprngimf1lem  21284  rngqiprngimf  21287  rng2idl1cntr  21295  znfld  21550  ipassr2  21637  ocvin  21664  pjfo  21705  obsne0  21715  frlmgsum  21762  aspval2  21888  psrlinv  21944  mplsubglem  21987  mpllsslem  21988  evlslem4  22064  evlslem1  22070  evlsval3  22077  mpfind  22103  evls1rhm  22297  madetsumid  22436  scmatcrng  22496  mdetleib2  22563  cramerimplem1  22658  m2pmfzgsumcl  22723  decpmatmul  22747  pmatcollpwscmat  22766  idpm2idmp  22776  pm2mpmhmlem1  22793  chpscmatgsummon  22820  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  topbas  22947  uncld  23016  incld  23018  elcls  23048  neiptopnei  23107  resttopon  23136  restdis  23153  cnclima  23243  paste  23269  cncmp  23367  clsconn  23405  conncompcld  23409  1stcfb  23420  2ndcsb  23424  2ndcredom  23425  kgencmp2  23521  txss12  23580  qtoptop2  23674  qtoptopon  23679  hmphindis  23772  uffixfr  23898  ufildr  23906  isfcls2  23988  tgplacthmeo  24078  tsmsgsum  24114  tgptsmscld  24126  tsmssplit  24127  ustuqtop5  24220  uspreg  24248  prdsxmetlem  24343  prdsbl  24466  metss  24483  metrest  24499  nrmmetd  24549  isngp2  24572  ngpsubcan  24589  lssnlm  24676  nmoid  24717  opnreen  24807  mpomulcn  24844  evth  24936  htpyco2  24956  phtpyco2  24967  clmvz  25088  tcphcph  25214  iscmet3  25270  metcld  25283  bcthlem2  25302  cssbn  25352  chlcsschl  25355  minveclem1  25401  evthicc2  25437  ovolunlem1a  25473  ovolicc2lem1  25494  ovolicc2lem4  25497  ovolicc2lem5  25498  uniioombllem2  25560  uniioombllem3  25562  vitalilem2  25586  vitalilem4  25588  vitalilem5  25589  itg2monolem1  25727  cpnres  25914  rolle  25967  dvlip2  25972  dvivthlem2  25986  dvfsumrlimge0  26007  deg1pwle  26095  plydivlem4  26273  ulm0  26369  efif1olem1  26519  efif1olem2  26520  eflogeq  26579  argimlt0  26590  logrec  26740  relogbcxp  26762  atanlogadd  26891  atanlogsub  26893  atantan  26900  ftalem4  27053  ftalem5  27054  basellem3  27060  chtub  27189  dchrpt  27244  dchrsum2  27245  gausslemma2dlem1a  27342  2lgslem3a1  27377  2lgslem3b1  27378  2lgslem3c1  27379  2lgslem3d1  27380  2lgsoddprm  27393  dchrisumlem2  27467  pntrsumbnd2  27544  nosupbnd1lem4  27689  noinfbnd2lem1  27708  cutbdaylt  27804  oldlim  27893  madebday  27906  cofcutr  27930  addbday  28024  negbdaylem  28062  absmuls  28250  absnegs  28253  bdayfinlem  28492  cnvmot  28623  tglineneq  28726  midexlem  28774  midex  28819  axlowdimlem14  29038  uhgrspansubgrlem  29373  usgrres  29391  usgrnbcnvfv  29448  finsumvtxdg2sstep  29633  uspgr2wlkeq  29729  redwlk  29754  pthdivtx  29810  usgr2wlkspthlem2  29841  wwlknvtx  29928  2wlkdlem6  30014  umgr2wlkon  30033  rusgrnumwwlk  30061  clwwlkwwlksb  30139  clwwlknwwlksnb  30140  clwwnisshclwwsn  30144  clwwlknscsh  30147  clwlknf1oclwwlknlem1  30166  1wlkdlem2  30223  fusgreghash2wsp  30423  2clwwlklem  30428  2clwwlk2clwwlk  30435  numclwwlk6  30475  prssad  32614  prssbd  32615  ofrn2  32728  ofpreima2  32754  sgnval2  32823  argcj  32836  wrdsplex  33011  ccatf1  33024  mgcf1o  33078  gsumfs2d  33137  gsumhashmul  33143  gsummulsubdishift1  33144  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmco2  33209  cyc3co2  33216  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnsubrunlem1  33323  erler  33341  fracerl  33382  imaslmod  33428  elrspunidl  33503  qsidomlem1  33527  qsidomlem2  33528  ssdifidllem  33531  ssdifidlprm  33533  ressply1evls1  33640  ply1coedeg  33664  esplyfval3  33731  exsslsb  33756  dimpropd  33768  lbsdiflsp0  33786  extdg1id  33826  madjusmdetlem2  33988  zarcmplem  34041  eulerpartlemgvv  34536  boolesineq  34615  fineqvnttrclselem1  35281  vonf1owev  35306  pfxwlk  35322  revwlk  35323  pthhashvtx  35326  spthcycl  35327  umgracycusgr  35352  subfacp1lem5  35382  satfvsucsuc  35563  ply1divalg3  35840  weiunfrlem  36662  ttctr  36691  dfttc2g  36704  cnambfre  38003  mapdordlem2  42097  frlmvscadiccat  42965  ricdrng1  42987  evlsbagval  43016  0prjspn  43075  3cubes  43136  oninfint  43682  onexomgt  43687  onexoegt  43690  ordeldif  43704  oacl2g  43776  onmcl  43777  omabs2  43778  omcl2  43779  tfsconcatfv  43787  tfsconcatrev  43794  ofoafg  43800  ofoafo  43802  ofoaass  43806  ofoacom  43807  onsucunifi  43816  oaun3lem1  43820  oadif1lem  43825  oadif1  43826  naddwordnexlem4  43847  safesnsupfilb  43863  gneispace  44579  rr-phpd  44654  grumnudlem  44730  ax6e2ndeqALT  45375  sineq0ALT  45381  fnresdmss  45616  saliinclf  46772  hoicvr  46994  setsv  47850  sprsymrelfolem2  47965  lighneal  48086  indprmfz  48105  grimuhgr  48375  grimcnv  48376  uhgrimedgi  48378  uhgrimedg  48379  isuspgrim0lem  48381  isuspgrim0  48382  upgrimtrlslem1  48392  upgrimtrlslem2  48393  clnbgrgrim  48422  grimedg  48423  isubgr3stgrlem8  48461  clnbgr3stgrgrlim  48507  clnbgr3stgrgrlic  48508  lincresunit3  48969  2itscp  49269  resccat  49561