Theorem syl2an2r 685

Description: syl2anr 597 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 580	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 591	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  5121  axprlem4OLD  5404  brcogw  5853  funfni  6649  f1un  6843  fvelimab  6956  dff3  7095  fnex  7214  ralima  7234  f1cofveqaeq  7255  f1eqcocnv  7299  caofid0l  7709  caofid0r  7710  caofid1  7711  caofid2  7712  onmindif2  7806  limsssuc  7850  mptcnfimad  7990  fnse  8137  frrlem13  8302  iinon  8359  smoord  8384  smoword  8385  tfrlem11  8407  coflton  8688  cofonr  8691  naddasslem2  8712  boxcutc  8960  f1domg  8991  phpeqd  9231  phpeqdOLD  9239  ominf  9271  f1finf1o  9282  findcard3OLD  9296  unfilem1  9320  f1opwfi  9373  marypha2  9456  supmax  9485  infmin  9513  ordtypelem6  9542  oiexg  9554  oien  9557  cantnff  9693  cantnfp1lem3  9699  cantnflem1b  9705  cantnflem1  9708  ttrcltr  9735  ttrclselem2  9745  opwf  9831  rankopb  9871  xpnum  9970  infxpenlem  10032  infxp  10233  cflim2  10282  cofsmo  10288  cfsmolem  10289  cfcoflem  10291  ssfin3ds  10349  isf34lem5  10397  isf34lem6  10399  isfin1-3  10405  axcc3  10457  alephval2  10591  fpwwe2lem7  10656  canthp1  10673  tsken  10773  ltaddpr  11053  dedekind  11403  recextlem2  11873  recex  11874  gt0div  12113  ge0div  12114  lerec2  12135  uzwo2  12933  infssuzcl  12953  qmulcl  12988  xnegdi  13269  xmulpnf1n  13299  xadddi2  13318  fzm1  13629  2submod  13955  addmodlteq  13969  expnlbnd  14256  faclbnd5  14321  hasheni  14371  hashdifpr  14438  hashgt23el  14447  ccatrn  14612  ccatalpha  14616  swrds1  14689  swrdccat2  14692  ccatpfx  14724  swrdccatin2  14752  pfxccatin12lem2  14754  revccat  14789  revrev  14790  swrdco  14861  relexpindlem  15087  resqrex  15274  fzomaxdiflem  15366  climconst  15564  serf0  15702  fsumf1o  15744  fsumrev  15800  fsumabs  15822  cvgcmp  15837  binomlem  15850  isumshft  15860  climcndslem1  15870  climcndslem2  15871  climcnds  15872  supcvg  15877  fprodcl2lem  15971  tanneg  16171  rpnnen2lem11  16247  modm1div  16289  fzo0dvdseq  16347  bitsfzolem  16458  gcdcllem3  16525  hashdvds  16799  prmdivdiv  16811  reumodprminv  16829  nnnn0modprm0  16831  pythagtrip  16859  dvdsprmpweqle  16911  pockthg  16931  4sqlem9  16971  vdwmc2  17004  vdwlem2  17007  imasaddflem  17549  acsfn1  17678  acsfn1c  17679  acsfn2  17680  oppccofval  17733  rescabs  17851  diag2  18262  grpinvalem  18656  issubmnd  18744  imasmnd  18758  pwsco2mhm  18816  gsumwspan  18829  frmdss2  18846  grpinvssd  19005  pwssub  19042  imasgrp  19044  subginv  19121  subginvcl  19123  ecqusaddcl  19181  ghmpreima  19226  conjnsg  19242  gass  19289  gsmsymgreqlem2  19417  f1omvdmvd  19429  symgsssg  19453  symgfisg  19454  symgtrinv  19458  psgnunilem5  19480  sylow1lem2  19585  odcau  19590  sylow2a  19605  sylow2  19612  efgsp1  19723  frgpuptf  19756  frgpuptinv  19757  frgpupf  19759  frgpup3lem  19763  mulgdi  19812  gsumval3eu  19890  gsumzsplit  19913  gsumzmhm  19923  gsumxp2  19966  prdsgsum  19967  fsfnn0gsumfsffz  19969  ablfaclem3  20075  srgbinomlem  20195  gsummgp0  20283  imasring  20295  dvdsr01  20336  rngisom1  20431  01eq0ring  20495  issubrng2  20523  subrgcrng  20540  subrginv  20553  isdrngd  20730  imadrhmcl  20762  abv1z  20789  lcomfsupp  20864  lmodvneg1  20867  lspsn  20964  lmhmco  21006  lmhmima  21010  lmhmpreima  21011  reslmhm  21015  lbsextlem2  21125  isridlrng  21185  lidl0cl  21186  elrspsn  21206  rnglidlmmgm  21211  rnglidlmsgrp  21212  2idlcpblrng  21237  quscrng  21249  rngqiprngghmlem1  21253  rngqiprngghmlem3  21255  rngqiprnglinlem3  21259  rngqiprngimf1lem  21260  rngqiprngimf  21263  rng2idl1cntr  21271  znfld  21526  ipassr2  21612  ocvin  21639  pjfo  21680  obsne0  21690  frlmgsum  21737  aspval2  21863  psrlinv  21920  mplsubglem  21964  mpllsslem  21965  evlslem4  22039  evlslem1  22045  mpfind  22070  evls1rhm  22265  madetsumid  22404  scmatcrng  22464  mdetleib2  22531  cramerimplem1  22626  m2pmfzgsumcl  22691  decpmatmul  22715  pmatcollpwscmat  22734  idpm2idmp  22744  pm2mpmhmlem1  22761  chpscmatgsummon  22788  chfacfscmulgsum  22803  chfacfpmmulgsum  22807  topbas  22915  uncld  22984  incld  22986  elcls  23016  neiptopnei  23075  resttopon  23104  restdis  23121  cnclima  23211  paste  23237  cncmp  23335  clsconn  23373  conncompcld  23377  1stcfb  23388  2ndcsb  23392  2ndcredom  23393  kgencmp2  23489  txss12  23548  qtoptop2  23642  qtoptopon  23647  hmphindis  23740  uffixfr  23866  ufildr  23874  isfcls2  23956  tgplacthmeo  24046  tsmsgsum  24082  tgptsmscld  24094  tsmssplit  24095  ustuqtop5  24189  uspreg  24217  prdsxmetlem  24312  prdsbl  24435  metss  24452  metrest  24468  nrmmetd  24518  isngp2  24541  ngpsubcan  24558  lssnlm  24645  nmoid  24686  opnreen  24776  mpomulcn  24814  evth  24914  htpyco2  24934  phtpyco2  24945  clmvz  25067  tcphcph  25194  iscmet3  25250  metcld  25263  bcthlem2  25282  cssbn  25332  chlcsschl  25335  minveclem1  25381  evthicc2  25418  ovolunlem1a  25454  ovolicc2lem1  25475  ovolicc2lem4  25478  ovolicc2lem5  25479  uniioombllem2  25541  uniioombllem3  25543  vitalilem2  25567  vitalilem4  25569  vitalilem5  25570  itg2monolem1  25708  cpnres  25896  rolle  25951  dvlip2  25957  dvivthlem2  25971  dvfsumrlimge0  25994  deg1pwle  26082  plydivlem4  26261  ulm0  26357  efif1olem1  26508  efif1olem2  26509  eflogeq  26568  argimlt0  26579  logrec  26730  relogbcxp  26752  atanlogadd  26881  atanlogsub  26883  atantan  26890  ftalem4  27043  ftalem5  27044  basellem3  27050  chtub  27180  dchrpt  27235  dchrsum2  27236  gausslemma2dlem1a  27333  2lgslem3a1  27368  2lgslem3b1  27369  2lgslem3c1  27370  2lgslem3d1  27371  2lgsoddprm  27384  dchrisumlem2  27458  pntrsumbnd2  27535  nosupbnd1lem4  27680  noinfbnd2lem1  27699  scutbdaylt  27787  oldlim  27855  madebday  27868  cofcutr  27889  addsbday  27981  negsbdaylem  28019  absmuls  28203  abssneg  28206  cnvmot  28525  tglineneq  28628  midexlem  28676  midex  28721  axlowdimlem14  28939  uhgrspansubgrlem  29274  usgrres  29292  usgrnbcnvfv  29349  finsumvtxdg2sstep  29534  uspgr2wlkeq  29631  redwlk  29657  pthdivtx  29714  usgr2wlkspthlem2  29745  wwlknvtx  29832  2wlkdlem6  29918  umgr2wlkon  29937  rusgrnumwwlk  29962  clwwlkwwlksb  30040  clwwlknwwlksnb  30041  clwwnisshclwwsn  30045  clwwlknscsh  30048  clwlknf1oclwwlknlem1  30067  1wlkdlem2  30124  fusgreghash2wsp  30324  2clwwlklem  30329  2clwwlk2clwwlk  30336  numclwwlk6  30376  prssad  32515  prssbd  32516  ofrn2  32623  ofpreima2  32649  sgnval2  32717  argcj  32731  wrdsplex  32916  ccatf1  32929  mgcf1o  32988  gsumfs2d  33054  gsumhashmul  33060  cycpmco2lem5  33146  cycpmco2lem6  33147  cycpmco2lem7  33148  cycpmco2  33149  cyc3co2  33156  elrgspnlem1  33242  elrgspnlem2  33243  elrgspnsubrunlem1  33247  erler  33265  fracerl  33305  imaslmod  33373  elrspunidl  33448  qsidomlem1  33472  qsidomlem2  33473  ssdifidllem  33476  ssdifidlprm  33478  ressply1evls1  33583  exsslsb  33641  dimpropd  33653  lbsdiflsp0  33671  extdg1id  33712  madjusmdetlem2  33864  zarcmplem  33917  eulerpartlemgvv  34413  boolesineq  34492  pfxwlk  35151  revwlk  35152  pthhashvtx  35155  spthcycl  35156  umgracycusgr  35181  subfacp1lem5  35211  satfvsucsuc  35392  ply1divalg3  35669  weiunfrlem  36487  cnambfre  37697  frlmvscadiccat  42504  ricdrng1  42526  pwsgprod  42542  evlsval3  42557  evlsbagval  42564  0prjspn  42626  3cubes  42688  oninfint  43235  onexomgt  43240  onexoegt  43243  ordeldif  43257  oacl2g  43329  onmcl  43330  omabs2  43331  omcl2  43332  tfsconcatfv  43340  tfsconcatrev  43347  ofoafg  43353  ofoafo  43355  ofoaass  43359  ofoacom  43360  onsucunifi  43369  oaun3lem1  43373  oadif1lem  43378  oadif1  43379  naddwordnexlem4  43400  safesnsupfilb  43417  gneispace  44133  rr-phpd  44208  grumnudlem  44284  ax6e2ndeqALT  44930  sineq0ALT  44936  fnresdmss  45172  saliinclf  46335  setsv  47372  sprsymrelfolem2  47487  lighneal  47605  grimuhgr  47880  grimcnv  47881  uhgrimedgi  47883  uhgrimedg  47884  isuspgrim0lem  47886  isuspgrim0  47887  upgrimtrlslem1  47897  upgrimtrlslem2  47898  clnbgrgrim  47927  grimedg  47928  isubgr3stgrlem8  47965  clnbgr3stgrgrlic  48004  lincresunit3  48437  2itscp  48741  resccat  49021