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  5090  axprlem4OLD  5369  brcogw  5812  funfni  6592  f1un  6788  fvelimab  6900  dff3  7039  fnex  7157  ralima  7177  f1cofveqaeq  7197  f1eqcocnv  7241  caofid0l  7649  caofid0r  7650  caofid1  7651  caofid2  7652  onmindif2  7746  limsssuc  7786  mptcnfimad  7924  fnse  8069  frrlem13  8234  iinon  8266  smoord  8291  smoword  8292  tfrlem11  8313  coflton  8592  cofonr  8595  naddasslem2  8616  boxcutc  8871  f1domg  8900  phpeqd  9128  ominf  9155  f1finf1o  9164  unfilem1  9196  f1opwfi  9247  marypha2  9330  supmax  9359  infmin  9387  ordtypelem6  9416  oiexg  9428  oien  9431  cantnff  9571  cantnfp1lem3  9577  cantnflem1b  9583  cantnflem1  9586  ttrcltr  9613  ttrclselem2  9623  opwf  9712  rankopb  9752  xpnum  9851  infxpenlem  9911  infxp  10112  cflim2  10161  cofsmo  10167  cfsmolem  10168  cfcoflem  10170  ssfin3ds  10228  isf34lem5  10276  isf34lem6  10278  isfin1-3  10284  axcc3  10336  alephval2  10470  fpwwe2lem7  10535  canthp1  10552  tsken  10652  ltaddpr  10932  dedekind  11283  recextlem2  11755  recex  11756  gt0div  11995  ge0div  11996  lerec2  12017  uzwo2  12812  infssuzcl  12832  qmulcl  12867  xnegdi  13149  xmulpnf1n  13179  xadddi2  13198  fzm1  13509  2submod  13841  addmodlteq  13855  expnlbnd  14142  faclbnd5  14207  hasheni  14257  hashdifpr  14324  hashgt23el  14333  ccatrn  14499  ccatalpha  14503  swrds1  14576  swrdccat2  14579  ccatpfx  14610  swrdccatin2  14638  pfxccatin12lem2  14640  revccat  14675  revrev  14676  swrdco  14746  relexpindlem  14972  resqrex  15159  fzomaxdiflem  15252  climconst  15452  serf0  15590  fsumf1o  15632  fsumrev  15688  fsumabs  15710  cvgcmp  15725  binomlem  15738  isumshft  15748  climcndslem1  15758  climcndslem2  15759  climcnds  15760  supcvg  15765  fprodcl2lem  15859  tanneg  16059  rpnnen2lem11  16135  modm1div  16177  fzo0dvdseq  16236  bitsfzolem  16347  gcdcllem3  16414  hashdvds  16688  prmdivdiv  16700  reumodprminv  16718  nnnn0modprm0  16720  pythagtrip  16748  dvdsprmpweqle  16800  pockthg  16820  4sqlem9  16860  vdwmc2  16893  vdwlem2  16896  imasaddflem  17436  acsfn1  17569  acsfn1c  17570  acsfn2  17571  oppccofval  17624  rescabs  17742  diag2  18153  grpinvalem  18583  issubmnd  18671  imasmnd  18685  pwsco2mhm  18743  gsumwspan  18756  frmdss2  18773  grpinvssd  18932  pwssub  18969  imasgrp  18971  subginv  19048  subginvcl  19050  ecqusaddcl  19107  ghmpreima  19152  conjnsg  19168  gass  19215  gsmsymgreqlem2  19345  f1omvdmvd  19357  symgsssg  19381  symgfisg  19382  symgtrinv  19386  psgnunilem5  19408  sylow1lem2  19513  odcau  19518  sylow2a  19533  sylow2  19540  efgsp1  19651  frgpuptf  19684  frgpuptinv  19685  frgpupf  19687  frgpup3lem  19691  mulgdi  19740  gsumval3eu  19818  gsumzsplit  19841  gsumzmhm  19851  gsumxp2  19894  prdsgsum  19895  fsfnn0gsumfsffz  19897  ablfaclem3  20003  srgbinomlem  20150  gsummgp0  20238  imasring  20250  dvdsr01  20291  rngisom1  20386  01eq0ring  20447  issubrng2  20475  subrgcrng  20492  subrginv  20505  isdrngd  20682  imadrhmcl  20714  abv1z  20741  lcomfsupp  20837  lmodvneg1  20840  lspsn  20937  lmhmco  20979  lmhmima  20983  lmhmpreima  20984  reslmhm  20988  lbsextlem2  21098  isridlrng  21158  lidl0cl  21159  elrspsn  21179  rnglidlmmgm  21184  rnglidlmsgrp  21185  2idlcpblrng  21210  quscrng  21222  rngqiprngghmlem1  21226  rngqiprngghmlem3  21228  rngqiprnglinlem3  21232  rngqiprngimf1lem  21233  rngqiprngimf  21236  rng2idl1cntr  21244  znfld  21499  ipassr2  21586  ocvin  21613  pjfo  21654  obsne0  21664  frlmgsum  21711  aspval2  21837  psrlinv  21894  mplsubglem  21937  mpllsslem  21938  evlslem4  22012  evlslem1  22018  mpfind  22043  evls1rhm  22238  madetsumid  22377  scmatcrng  22437  mdetleib2  22504  cramerimplem1  22599  m2pmfzgsumcl  22664  decpmatmul  22688  pmatcollpwscmat  22707  idpm2idmp  22717  pm2mpmhmlem1  22734  chpscmatgsummon  22761  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  topbas  22888  uncld  22957  incld  22959  elcls  22989  neiptopnei  23048  resttopon  23077  restdis  23094  cnclima  23184  paste  23210  cncmp  23308  clsconn  23346  conncompcld  23350  1stcfb  23361  2ndcsb  23365  2ndcredom  23366  kgencmp2  23462  txss12  23521  qtoptop2  23615  qtoptopon  23620  hmphindis  23713  uffixfr  23839  ufildr  23847  isfcls2  23929  tgplacthmeo  24019  tsmsgsum  24055  tgptsmscld  24067  tsmssplit  24068  ustuqtop5  24161  uspreg  24189  prdsxmetlem  24284  prdsbl  24407  metss  24424  metrest  24440  nrmmetd  24490  isngp2  24513  ngpsubcan  24530  lssnlm  24617  nmoid  24658  opnreen  24748  mpomulcn  24786  evth  24886  htpyco2  24906  phtpyco2  24917  clmvz  25039  tcphcph  25165  iscmet3  25221  metcld  25234  bcthlem2  25253  cssbn  25303  chlcsschl  25306  minveclem1  25352  evthicc2  25389  ovolunlem1a  25425  ovolicc2lem1  25446  ovolicc2lem4  25449  ovolicc2lem5  25450  uniioombllem2  25512  uniioombllem3  25514  vitalilem2  25538  vitalilem4  25540  vitalilem5  25541  itg2monolem1  25679  cpnres  25867  rolle  25922  dvlip2  25928  dvivthlem2  25942  dvfsumrlimge0  25965  deg1pwle  26053  plydivlem4  26232  ulm0  26328  efif1olem1  26479  efif1olem2  26480  eflogeq  26539  argimlt0  26550  logrec  26701  relogbcxp  26723  atanlogadd  26852  atanlogsub  26854  atantan  26861  ftalem4  27014  ftalem5  27015  basellem3  27021  chtub  27151  dchrpt  27206  dchrsum2  27207  gausslemma2dlem1a  27304  2lgslem3a1  27339  2lgslem3b1  27340  2lgslem3c1  27341  2lgslem3d1  27342  2lgsoddprm  27355  dchrisumlem2  27429  pntrsumbnd2  27506  nosupbnd1lem4  27651  noinfbnd2lem1  27670  scutbdaylt  27760  oldlim  27833  madebday  27846  cofcutr  27869  addsbday  27961  negsbdaylem  27999  absmuls  28183  abssneg  28186  cnvmot  28520  tglineneq  28623  midexlem  28671  midex  28716  axlowdimlem14  28935  uhgrspansubgrlem  29270  usgrres  29288  usgrnbcnvfv  29345  finsumvtxdg2sstep  29530  uspgr2wlkeq  29626  redwlk  29651  pthdivtx  29707  usgr2wlkspthlem2  29738  wwlknvtx  29825  2wlkdlem6  29911  umgr2wlkon  29930  rusgrnumwwlk  29958  clwwlkwwlksb  30036  clwwlknwwlksnb  30037  clwwnisshclwwsn  30041  clwwlknscsh  30044  clwlknf1oclwwlknlem1  30063  1wlkdlem2  30120  fusgreghash2wsp  30320  2clwwlklem  30325  2clwwlk2clwwlk  30332  numclwwlk6  30372  prssad  32511  prssbd  32512  ofrn2  32624  ofpreima2  32650  sgnval2  32722  argcj  32736  wrdsplex  32924  ccatf1  32937  mgcf1o  32991  gsumfs2d  33042  gsumhashmul  33048  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmco2  33109  cyc3co2  33116  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnsubrunlem1  33221  erler  33239  fracerl  33279  imaslmod  33325  elrspunidl  33400  qsidomlem1  33424  qsidomlem2  33425  ssdifidllem  33428  ssdifidlprm  33430  ressply1evls1  33535  esplyfval3  33612  exsslsb  33630  dimpropd  33642  lbsdiflsp0  33660  extdg1id  33700  madjusmdetlem2  33862  zarcmplem  33915  eulerpartlemgvv  34410  boolesineq  34489  fineqvnttrclselem1  35162  vonf1owev  35173  pfxwlk  35189  revwlk  35190  pthhashvtx  35193  spthcycl  35194  umgracycusgr  35219  subfacp1lem5  35249  satfvsucsuc  35430  ply1divalg3  35707  weiunfrlem  36529  cnambfre  37728  mapdordlem2  41756  frlmvscadiccat  42624  ricdrng1  42646  pwsgprod  42662  evlsval3  42677  evlsbagval  42684  0prjspn  42746  3cubes  42807  oninfint  43353  onexomgt  43358  onexoegt  43361  ordeldif  43375  oacl2g  43447  onmcl  43448  omabs2  43449  omcl2  43450  tfsconcatfv  43458  tfsconcatrev  43465  ofoafg  43471  ofoafo  43473  ofoaass  43477  ofoacom  43478  onsucunifi  43487  oaun3lem1  43491  oadif1lem  43496  oadif1  43497  naddwordnexlem4  43518  safesnsupfilb  43535  gneispace  44251  rr-phpd  44326  grumnudlem  44402  ax6e2ndeqALT  45047  sineq0ALT  45053  fnresdmss  45289  saliinclf  46448  setsv  47502  sprsymrelfolem2  47617  lighneal  47735  grimuhgr  48011  grimcnv  48012  uhgrimedgi  48014  uhgrimedg  48015  isuspgrim0lem  48017  isuspgrim0  48018  upgrimtrlslem1  48028  upgrimtrlslem2  48029  clnbgrgrim  48058  grimedg  48059  isubgr3stgrlem8  48097  clnbgr3stgrgrlim  48143  clnbgr3stgrgrlic  48144  lincresunit3  48606  2itscp  48906  resccat  49199