Theorem syl2an2r 697

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5107  axprlem4OLD  5403  brcogw  5856  funfni  6643  f1un  6843  fvelimab  6955  dff3  7097  fnex  7217  ralima  7237  f1cofveqaeq  7257  f1eqcocnv  7301  caofid0l  7709  caofid0r  7710  caofid1  7711  caofid2  7712  onmindif2  7807  limsssuc  7847  mptcnfimad  7984  fnse  8130  frrlem13  8296  iinon  8328  smoord  8353  smoword  8354  tfrlem11  8376  coflton  8658  cofonr  8661  naddasslem2  8683  boxcutc  8940  f1domg  8969  phpeqd  9197  ominf  9225  f1finf1o  9234  unfilem1  9266  f1opwfi  9314  marypha2  9400  supmax  9429  infmin  9457  ordtypelem6  9486  oiexg  9498  oien  9501  cantnff  9644  cantnfp1lem3  9650  cantnflem1b  9656  cantnflem1  9659  ttrcltr  9686  ttrclselem2  9696  opwf  9785  rankopb  9825  xpnum  9938  infxpenlem  9998  infxp  10198  cflim2  10248  cofsmo  10254  cfsmolem  10255  cfcoflem  10257  ssfin3ds  10315  isf34lem5  10363  isf34lem6  10365  isfin1-3  10371  axcc3  10423  alephval2  10558  fpwwe2lem7  10623  canthp1  10640  tsken  10740  ltaddpr  11020  dedekind  11374  recextlem2  11846  recex  11847  gt0div  12082  ge0div  12083  lerec2  12104  uzwo2  12937  infssuzcl  12957  qmulcl  12992  xnegdi  13275  xmulpnf1n  13305  xadddi2  13324  fzm1  13637  2submod  13970  addmodlteq  13984  expnlbnd  14271  faclbnd5  14336  hasheni  14386  hashdifpr  14454  hashgt23el  14463  ccatrn  14629  ccatalpha  14633  swrds1  14706  swrdccat2  14709  ccatpfx  14740  swrdccatin2  14768  pfxccatin12lem2  14770  revccat  14805  revrev  14806  swrdco  14876  relexpindlem  15102  resqrex  15303  fzomaxdiflem  15396  climconst  15596  serf0  15734  fsumf1o  15776  fsumrev  15832  fsumabs  15855  cvgcmp  15870  binomlem  15885  isumshft  15895  climcndslem1  15905  climcndslem2  15906  climcnds  15907  supcvg  15912  fprodcl2lem  16006  tanneg  16205  rpnnen2lem11  16281  modm1div  16323  fzo0dvdseq  16382  bitsfzolem  16493  gcdcllem3  16560  hashdvds  16835  prmdivdiv  16847  reumodprminv  16865  nnnn0modprm0  16867  pythagtrip  16895  dvdsprmpweqle  16947  pockthg  16967  4sqlem9  17007  vdwmc2  17040  vdwlem2  17043  imasaddflem  17585  acsfn1  17718  acsfn1c  17719  acsfn2  17720  oppccofval  17773  rescabs  17891  diag2  18302  grpinvalem  18732  issubmnd  18820  imasmnd  18834  pwsco2mhm  18893  gsumwspan  18906  frmdss2  18923  grpinvssd  19084  pwssub  19121  imasgrp  19123  subginv  19200  subginvcl  19202  ecqusaddcl  19265  ghmpreima  19309  conjnsg  19325  gass  19372  gsmsymgreqlem2  19502  f1omvdmvd  19514  symgsssg  19538  symgfisg  19539  symgtrinv  19543  psgnunilem5  19565  sylow1lem2  19670  odcau  19675  sylow2a  19690  sylow2  19697  efgsp1  19808  frgpuptf  19841  frgpuptinv  19842  frgpupf  19844  frgpup3lem  19848  mulgdi  19897  gsumval3eu  19975  gsumzsplit  19998  gsumzmhm  20008  gsumxp2  20051  prdsgsum  20052  fsfnn0gsumfsffz  20054  ablfaclem3  20160  srgbinomlem  20313  gsummgp0  20400  pwsgprod  20412  imasring  20413  dvdsr01  20454  rngisom1  20549  01eq0ring  20615  issubrng2  20644  subrgcrng  20661  subrginv  20674  isdrngd  20850  imadrhmcl  20881  abv1z  20908  lcomfsupp  21004  lmodvneg1  21007  lspsn  21104  lmhmco  21145  lmhmima  21149  lmhmpreima  21150  reslmhm  21154  lbsextlem2  21264  isridlrng  21325  lidl0cl  21326  lidlunin0  21342  rspvalint  21350  elrspsn  21352  rnglidlmmgm  21360  rnglidlmsgrp  21361  2idlcpblrng  21391  quscrng  21404  rngqiprngghmlem1  21408  rngqiprngghmlem3  21410  rngqiprnglinlem3  21414  rngqiprngimf1lem  21415  rngqiprngimf  21418  rng2idl1cntr  21426  qsidomlem1  21461  qsidomlem2  21462  ssdifidllem  21465  ssdifidlprm  21467  znfld  21691  ipassr2  21778  ocvin  21805  pjfo  21846  obsne0  21856  frlmgsum  21903  aspval2  22029  psrlinv  22086  mplsubglem  22129  mpllsslem  22130  evlslem4  22208  evlslem1  22214  evlsval3  22221  mpfind  22247  evls1rhm  22463  madetsumid  22599  scmatcrng  22659  mdetleib2  22726  cramerimplem1  22821  m2pmfzgsumcl  22886  decpmatmul  22910  pmatcollpwscmat  22929  idpm2idmp  22939  pm2mpmhmlem1  22956  chpscmatgsummon  22983  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  topbas  23110  uncld  23179  incld  23181  elcls  23211  neiptopnei  23270  resttopon  23299  restdis  23316  cnclima  23406  paste  23432  cncmp  23530  clsconn  23568  conncompcld  23572  1stcfb  23583  2ndcsb  23587  2ndcredom  23588  kgencmp2  23684  txss12  23743  qtoptop2  23837  qtoptopon  23842  hmphindis  23935  uffixfr  24061  ufildr  24069  isfcls2  24151  tgplacthmeo  24241  tsmsgsum  24277  tgptsmscld  24289  tsmssplit  24290  ustuqtop5  24383  uspreg  24411  prdsxmetlem  24506  prdsbl  24629  metss  24646  metrest  24662  nrmmetd  24712  isngp2  24735  ngpsubcan  24752  lssnlm  24839  nmoid  24880  opnreen  24970  mpomulcn  25007  evth  25099  htpyco2  25119  phtpyco2  25130  clmvz  25251  tcphcph  25377  iscmet3  25433  metcld  25446  bcthlem2  25465  cssbn  25515  chlcsschl  25518  minveclem1  25564  evthicc2  25600  ovolunlem1a  25636  ovolicc2lem1  25657  ovolicc2lem4  25660  ovolicc2lem5  25661  uniioombllem2  25723  uniioombllem3  25725  vitalilem2  25749  vitalilem4  25751  vitalilem5  25752  itg2monolem1  25890  cpnres  26077  rolle  26130  dvlip2  26135  dvivthlem2  26149  dvfsumrlimge0  26170  deg1pwle  26258  plydivlem4  26438  ulm0  26535  efif1olem1  26688  efif1olem2  26689  eflogeq  26748  argimlt0  26759  logrec  26909  relogbcxp  26931  atanlogadd  27060  atanlogsub  27062  atantan  27069  ftalem4  27221  ftalem5  27222  basellem3  27228  chtub  27357  dchrpt  27412  dchrsum2  27413  gausslemma2dlem1a  27510  2lgslem3a1  27545  2lgslem3b1  27546  2lgslem3c1  27547  2lgslem3d1  27548  2lgsoddprm  27561  dchrisumlem2  27635  pntrsumbnd2  27712  nosupbnd1lem4  27856  noinfbnd2lem1  27875  cutbdaylt  27972  oldlim  28061  madebday  28074  cofcutr  28098  addbday  28192  negbdaylem  28230  absmuls  28418  absnegs  28421  bdayfinlem  28660  cnvmot  28791  tglineneq  28899  midexlem  28950  midex  28999  plngrotlem1  29050  axlowdimlem14  29286  uhgrspansubgrlem  29621  usgrres  29639  usgrnbcnvfv  29696  finsumvtxdg2sstep  29880  uspgr2wlkeq  29976  redwlk  30001  pthdivtx  30057  usgr2wlkspthlem2  30088  wwlknvtx  30175  2wlkdlem6  30261  umgr2wlkon  30280  rusgrnumwwlk  30308  clwwlkwwlksb  30386  clwwlknwwlksnb  30387  clwwnisshclwwsn  30391  clwwlknscsh  30394  clwlknf1oclwwlknlem1  30413  1wlkdlem2  30470  fusgreghash2wsp  30670  2clwwlklem  30675  2clwwlk2clwwlk  30682  numclwwlk6  30722  prssad  32856  prssbd  32857  ofrn2  32966  ofpreima2  32992  sgnval2  33061  argcj  33074  wrdsplex  33237  ccatf1  33250  mgcf1o  33304  gsumfs2d  33362  gsumhashmul  33368  gsummulsubdishift1  33369  cycpmco2lem5  33431  cycpmco2lem6  33432  cycpmco2lem7  33433  cycpmco2  33434  cyc3co2  33441  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnsubrunlem1  33548  erler  33566  fracerl  33608  imaslmod  33654  elrspunidl  33717  ressply1evls1  33836  ply1coedeg  33860  esplyfval3  33943  exsslsb  33968  dimpropd  33980  lbsdiflsp0  33997  extdg1id  34037  madjusmdetlem2  34199  zarcmplem  34252  eulerpartlemgvv  34747  boolesineq  34826  fineqvnttrclselem1  35515  vonf1wev  35573  vonf1owevOLD  35575  pfxwlk  35597  revwlk  35598  pthhashvtx  35601  spthcycl  35602  umgracycusgr  35627  subfacp1lem5  35657  satfvsucsuc  35838  ply1divalg3  36115  weiunfrlem  36956  ttctr  36985  dfttc2g  36998  cnambfre  38300  mapdordlem2  42392  frlmvscadiccat  43261  ricdrng1  43279  evlsbagval  43301  0prjspn  43343  3cubes  43404  oninfint  43946  onexomgt  43951  onexoegt  43954  ordeldif  43968  oacl2g  44040  onmcl  44041  omabs2  44042  omcl2  44043  tfsconcatfv  44051  tfsconcatrev  44058  ofoafg  44064  ofoafo  44066  ofoaass  44070  ofoacom  44071  onsucunifi  44080  oaun3lem1  44084  oadif1lem  44089  oadif1  44090  naddwordnexlem4  44111  safesnsupfilb  44127  gneispace  44843  rr-phpd  44916  grumnudlem  44978  ax6e2ndeqALT  45622  sineq0ALT  45628  hashnnlt  45714  fnresdmss  45869  saliinclf  47023  hoicvr  47245  setsv  48110  sprsymrelfolem2  48225  lighneal  48346  indprmfz  48365  grimuhgr  48635  grimcnv  48636  uhgrimedgi  48638  uhgrimedg  48639  isuspgrim0lem  48641  isuspgrim0  48642  upgrimtrlslem1  48652  upgrimtrlslem2  48653  clnbgrgrim  48682  grimedg  48683  isubgr3stgrlem8  48721  clnbgr3stgrgrlim  48767  clnbgr3stgrgrlic  48768  lincresunit3  49244  2itscp  49544  resccat  49835