Theorem syl2an2r 682

Description: syl2anr 596 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 579	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5	1, 4	syldan 590	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 206  df-an 396

This theorem is referenced by:  disjxiun  5145  axprlem4  5424  brcogw  5868  funfni  6655  f1un  6853  fvelimab  6964  dff3  7101  fnex  7221  f1cofveqaeq  7260  f1eqcocnv  7302  f1eqcocnvOLD  7303  caofid0l  7705  caofid0r  7706  caofid1  7707  caofid2  7708  onmindif2  7799  limsssuc  7843  fnse  8124  frrlem13  8289  iinon  8346  smoord  8371  smoword  8372  tfrlem11  8394  coflton  8676  cofonr  8679  naddasslem2  8700  boxcutc  8941  f1domg  8974  phpeqd  9221  phpeqdOLD  9231  ominf  9264  f1finf1o  9277  findcard3OLD  9292  unfilem1  9316  f1opwfi  9362  marypha2  9440  supmax  9468  infmin  9495  ordtypelem6  9524  oiexg  9536  oien  9539  cantnff  9675  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1  9690  ttrcltr  9717  ttrclselem2  9727  opwf  9813  rankopb  9853  xpnum  9952  infxpenlem  10014  infxp  10216  cflim2  10264  cofsmo  10270  cfsmolem  10271  cfcoflem  10273  ssfin3ds  10331  isf34lem5  10379  isf34lem6  10381  isfin1-3  10387  axcc3  10439  alephval2  10573  fpwwe2lem7  10638  canthp1  10655  tsken  10755  ltaddpr  11035  dedekind  11384  recextlem2  11852  recex  11853  gt0div  12087  ge0div  12088  lerec2  12109  uzwo2  12903  infssuzcl  12923  qmulcl  12958  xnegdi  13234  xmulpnf1n  13264  xadddi2  13283  fzm1  13588  2submod  13904  addmodlteq  13918  expnlbnd  14203  faclbnd5  14265  hasheni  14315  hashdifpr  14382  hashgt23el  14391  ccatrn  14546  ccatalpha  14550  swrds1  14623  swrdccat2  14626  ccatpfx  14658  swrdccatin2  14686  pfxccatin12lem2  14688  revccat  14723  revrev  14724  swrdco  14795  relexpindlem  15017  resqrex  15204  fzomaxdiflem  15296  climconst  15494  serf0  15634  fsumf1o  15676  fsumrev  15732  fsumabs  15754  cvgcmp  15769  binomlem  15782  isumshft  15792  climcndslem1  15802  climcndslem2  15803  climcnds  15804  supcvg  15809  fprodcl2lem  15901  tanneg  16098  rpnnen2lem11  16174  modm1div  16216  fzo0dvdseq  16273  bitsfzolem  16382  gcdcllem3  16449  hashdvds  16715  prmdivdiv  16727  reumodprminv  16744  nnnn0modprm0  16746  pythagtrip  16774  dvdsprmpweqle  16826  pockthg  16846  4sqlem9  16886  vdwmc2  16919  vdwlem2  16922  imasaddflem  17483  acsfn1  17612  acsfn1c  17613  acsfn2  17614  oppccofval  17668  rescabs  17789  diag2  18208  grprinvlem  18604  issubmnd  18692  imasmnd  18703  pwsco2mhm  18756  gsumwspan  18769  frmdss2  18786  grpinvssd  18943  pwssub  18980  imasgrp  18982  subginv  19056  subginvcl  19058  ecqusaddcl  19115  ghmpreima  19159  conjnsg  19175  gass  19213  gsmsymgreqlem2  19347  f1omvdmvd  19359  symgsssg  19383  symgfisg  19384  symgtrinv  19388  psgnunilem5  19410  sylow1lem2  19515  odcau  19520  sylow2a  19535  sylow2  19542  efgsp1  19653  frgpuptf  19686  frgpuptinv  19687  frgpupf  19689  frgpup3lem  19693  mulgdi  19742  gsumval3eu  19820  gsumzsplit  19843  gsumzmhm  19853  gsumxp2  19896  prdsgsum  19897  fsfnn0gsumfsffz  19899  ablfaclem3  20005  srgbinomlem  20131  gsummgp0  20213  imasring  20225  dvdsr01  20269  rngisom1  20364  01eq0ring  20426  issubrng2  20454  subrgcrng  20473  subrginv  20486  isdrngd  20616  imadrhmcl  20644  abv1z  20671  lcomfsupp  20744  lmodvneg1  20747  lspsn  20845  lmhmco  20887  lmhmima  20891  lmhmpreima  20892  reslmhm  20896  lbsextlem2  21006  isridlrng  21074  lidl0cl  21075  rnglidlmmgm  21099  rnglidlmsgrp  21100  2idlcpblrng  21124  quscrng  21134  rngqiprngghmlem1  21136  rngqiprngghmlem3  21138  rngqiprnglinlem3  21142  rngqiprngimf1lem  21143  rngqiprngimf  21146  rng2idl1cntr  21154  znfld  21427  ipassr2  21511  ocvin  21538  pjfo  21581  obsne0  21591  frlmgsum  21638  aspval2  21763  psrlinv  21828  mplsubglem  21870  mpllsslem  21871  evlslem4  21949  evlslem1  21957  mpfind  21982  evls1rhm  22162  madetsumid  22284  scmatcrng  22344  mdetleib2  22411  cramerimplem1  22506  m2pmfzgsumcl  22571  decpmatmul  22595  pmatcollpwscmat  22614  idpm2idmp  22624  pm2mpmhmlem1  22641  chpscmatgsummon  22668  chfacfscmulgsum  22683  chfacfpmmulgsum  22687  topbas  22796  uncld  22866  incld  22868  elcls  22898  neiptopnei  22957  resttopon  22986  restdis  23003  cnclima  23093  paste  23119  cncmp  23217  clsconn  23255  conncompcld  23259  1stcfb  23270  2ndcsb  23274  2ndcredom  23275  kgencmp2  23371  txss12  23430  qtoptop2  23524  qtoptopon  23529  hmphindis  23622  uffixfr  23748  ufildr  23756  isfcls2  23838  tgplacthmeo  23928  tsmsgsum  23964  tgptsmscld  23976  tsmssplit  23977  ustuqtop5  24071  uspreg  24100  prdsxmetlem  24195  prdsbl  24321  metss  24338  metrest  24354  nrmmetd  24404  isngp2  24427  ngpsubcan  24444  lssnlm  24539  nmoid  24580  opnreen  24668  mpomulcn  24706  evth  24806  htpyco2  24826  phtpyco2  24837  clmvz  24959  tcphcph  25086  iscmet3  25142  metcld  25155  bcthlem2  25174  cssbn  25224  chlcsschl  25227  minveclem1  25273  evthicc2  25310  ovolunlem1a  25346  ovolicc2lem1  25367  ovolicc2lem4  25370  ovolicc2lem5  25371  uniioombllem2  25433  uniioombllem3  25435  vitalilem2  25459  vitalilem4  25461  vitalilem5  25462  itg2monolem1  25601  cpnres  25788  rolle  25843  dvlip2  25849  dvivthlem2  25863  dvfsumrlimge0  25886  deg1pwle  25976  plydivlem4  26149  ulm0  26243  efif1olem1  26392  efif1olem2  26393  eflogeq  26451  argimlt0  26462  logrec  26610  relogbcxp  26632  atanlogadd  26761  atanlogsub  26763  atantan  26770  ftalem4  26923  ftalem5  26924  basellem3  26930  chtub  27060  dchrpt  27115  dchrsum2  27116  gausslemma2dlem1a  27213  2lgslem3a1  27248  2lgslem3b1  27249  2lgslem3c1  27250  2lgslem3d1  27251  2lgsoddprm  27264  dchrisumlem2  27338  pntrsumbnd2  27415  nosupbnd1lem4  27559  noinfbnd2lem1  27578  scutbdaylt  27666  oldlim  27728  madebday  27741  cofcutr  27759  negsbdaylem  27883  absmuls  28053  abssneg  28056  cnvmot  28227  tglineneq  28330  midexlem  28378  midex  28423  axlowdimlem14  28648  uhgrspansubgrlem  28982  usgrres  29000  usgrnbcnvfv  29057  finsumvtxdg2sstep  29241  uspgr2wlkeq  29338  redwlk  29364  pthdivtx  29421  usgr2wlkspthlem2  29450  wwlknvtx  29534  2wlkdlem6  29620  umgr2wlkon  29639  rusgrnumwwlk  29664  clwwlkwwlksb  29742  clwwlknwwlksnb  29743  clwwnisshclwwsn  29747  clwwlknscsh  29750  clwlknf1oclwwlknlem1  29769  1wlkdlem2  29826  fusgreghash2wsp  30026  2clwwlklem  30031  2clwwlk2clwwlk  30038  numclwwlk6  30078  ofrn2  32300  ofpreima2  32326  wrdsplex  32539  ccatf1  32550  mgcf1o  32608  gsumhashmul  32646  cycpmco2lem5  32727  cycpmco2lem6  32728  cycpmco2lem7  32729  cycpmco2  32730  cyc3co2  32737  imaslmod  32906  rspsnel  32926  elrspunidl  32988  qsidomlem1  33013  qsidomlem2  33014  dimpropd  33149  lbsdiflsp0  33167  extdg1id  33198  zarcmplem  33327  eulerpartlemgvv  33841  pfxwlk  34580  revwlk  34581  pthhashvtx  34584  spthcycl  34586  umgracycusgr  34611  subfacp1lem5  34641  satfvsucsuc  34822  cnambfre  37003  frlmvscadiccat  41550  ricdrng1  41570  pwsgprod  41580  evlsval3  41597  evlsbagval  41604  0prjspn  41836  3cubes  41894  oninfint  42451  onexomgt  42456  onexoegt  42459  ordeldif  42474  oacl2g  42546  onmcl  42547  omabs2  42548  omcl2  42549  tfsconcatfv  42557  tfsconcatrev  42564  ofoafg  42570  ofoafo  42572  ofoaass  42576  ofoacom  42577  onsucunifi  42586  oaun3lem1  42590  oadif1lem  42595  oadif1  42596  naddwordnexlem4  42618  safesnsupfilb  42635  gneispace  43351  rr-phpd  43428  grumnudlem  43510  ax6e2ndeqALT  44158  sineq0ALT  44164  fnresdmss  44329  saliinclf  45504  setsv  46508  sprsymrelfolem2  46623  lighneal  46741  isomuspgrlem2c  46960  lincresunit3  47327  2itscp  47632