Theorem syl2an2r 681

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  5075  axprlem4  5352  brcogw  5774  funfni  6535  fvelimab  6835  dff3  6970  fnex  7087  f1cofveqaeq  7125  f1eqcocnv  7166  f1eqcocnvOLD  7167  caofid0l  7555  caofid0r  7556  caofid1  7557  caofid2  7558  onmindif2  7647  limsssuc  7685  fnse  7958  frrlem13  8098  iinon  8155  smoord  8180  smoword  8181  tfrlem11  8203  boxcutc  8703  f1domg  8731  phpeqd  8962  phpeqdOLD  8973  findcard3  9018  unfilem1  9039  f1opwfi  9084  marypha2  9159  supmax  9187  infmin  9214  ordtypelem6  9243  oiexg  9255  oien  9258  cantnff  9393  cantnfp1lem3  9399  cantnflem1b  9405  cantnflem1  9408  ttrcltr  9435  ttrclselem2  9445  opwf  9554  rankopb  9594  xpnum  9693  infxpenlem  9753  infxp  9955  cflim2  10003  cofsmo  10009  cfsmolem  10010  cfcoflem  10012  ssfin3ds  10070  isf34lem5  10118  isf34lem6  10120  isfin1-3  10126  axcc3  10178  alephval2  10312  fpwwe2lem7  10377  canthp1  10394  tsken  10494  ltaddpr  10774  dedekind  11121  recextlem2  11589  recex  11590  gt0div  11824  ge0div  11825  lerec2  11846  uzwo2  12634  infssuzcl  12654  qmulcl  12689  xnegdi  12964  xmulpnf1n  12994  xadddi2  13013  fzm1  13318  2submod  13633  addmodlteq  13647  expnlbnd  13929  faclbnd5  13993  hasheni  14043  hashdifpr  14111  hashgt23el  14120  ccatrn  14275  ccatalpha  14279  swrds1  14360  swrdccat2  14363  ccatpfx  14395  swrdccatin2  14423  pfxccatin12lem2  14425  revccat  14460  revrev  14461  swrdco  14531  relexpindlem  14755  resqrex  14943  fzomaxdiflem  15035  climconst  15233  serf0  15373  fsumf1o  15416  fsumrev  15472  fsumabs  15494  cvgcmp  15509  binomlem  15522  isumshft  15532  climcndslem1  15542  climcndslem2  15543  climcnds  15544  supcvg  15549  fprodcl2lem  15641  tanneg  15838  rpnnen2lem11  15914  modm1div  15956  fzo0dvdseq  16013  bitsfzolem  16122  gcdcllem3  16189  hashdvds  16457  prmdivdiv  16469  reumodprminv  16486  nnnn0modprm0  16488  pythagtrip  16516  dvdsprmpweqle  16568  pockthg  16588  4sqlem9  16628  vdwmc2  16661  vdwlem2  16664  imasaddflem  17222  acsfn1  17351  acsfn1c  17352  acsfn2  17353  oppccofval  17407  rescabs  17528  diag2  17944  grprinvlem  18338  issubmnd  18393  imasmnd  18404  pwsco2mhm  18452  gsumwspan  18466  frmdss2  18483  grpinvssd  18633  pwssub  18670  imasgrp  18672  subginv  18743  subginvcl  18745  ghmpreima  18837  conjnsg  18851  gass  18888  gsmsymgreqlem2  19020  f1omvdmvd  19032  symgsssg  19056  symgfisg  19057  symgtrinv  19061  psgnunilem5  19083  sylow1lem2  19185  odcau  19190  sylow2a  19205  sylow2  19212  efgsp1  19324  frgpuptf  19357  frgpuptinv  19358  frgpupf  19360  frgpup3lem  19364  mulgdi  19409  gsumval3eu  19486  gsumzsplit  19509  gsumzmhm  19519  gsumxp2  19562  prdsgsum  19563  fsfnn0gsumfsffz  19565  ablfaclem3  19671  srgbinomlem  19761  gsummgp0  19828  imasring  19839  dvdsr01  19878  subrgcrng  20009  subrginv  20021  abv1z  20073  lcomfsupp  20144  lmodvneg1  20147  lspsn  20245  lmhmco  20286  lmhmima  20290  lmhmpreima  20291  reslmhm  20295  lbsextlem2  20402  lidl0cl  20464  znfld  20749  ipassr2  20833  ocvin  20860  pjfo  20903  obsne0  20913  frlmgsum  20960  aspval2  21083  psrlinv  21147  mplsubglem  21186  mpllsslem  21187  evlslem4  21265  evlslem1  21273  mpfind  21298  evls1rhm  21469  madetsumid  21591  scmatcrng  21651  mdetleib2  21718  cramerimplem1  21813  m2pmfzgsumcl  21878  decpmatmul  21902  pmatcollpwscmat  21921  idpm2idmp  21931  pm2mpmhmlem1  21948  chpscmatgsummon  21975  chfacfscmulgsum  21990  chfacfpmmulgsum  21994  topbas  22103  uncld  22173  incld  22175  elcls  22205  neiptopnei  22264  resttopon  22293  restdis  22310  cnclima  22400  paste  22426  cncmp  22524  clsconn  22562  conncompcld  22566  1stcfb  22577  2ndcsb  22581  2ndcredom  22582  kgencmp2  22678  txss12  22737  qtoptop2  22831  qtoptopon  22836  hmphindis  22929  uffixfr  23055  ufildr  23063  isfcls2  23145  tgplacthmeo  23235  tsmsgsum  23271  tgptsmscld  23283  tsmssplit  23284  ustuqtop5  23378  uspreg  23407  prdsxmetlem  23502  prdsbl  23628  metss  23645  metrest  23661  nrmmetd  23711  isngp2  23734  ngpsubcan  23751  lssnlm  23846  nmoid  23887  opnreen  23975  evth  24103  htpyco2  24123  phtpyco2  24134  clmvz  24255  tcphcph  24382  iscmet3  24438  metcld  24451  bcthlem2  24470  cssbn  24520  chlcsschl  24523  minveclem1  24569  evthicc2  24605  ovolunlem1a  24641  ovolicc2lem1  24662  ovolicc2lem4  24665  ovolicc2lem5  24666  uniioombllem2  24728  uniioombllem3  24730  vitalilem2  24754  vitalilem4  24756  vitalilem5  24757  itg2monolem1  24896  cpnres  25082  rolle  25135  dvlip2  25140  dvivthlem2  25154  dvfsumrlimge0  25175  deg1pwle  25265  plydivlem4  25437  ulm0  25531  efif1olem1  25679  efif1olem2  25680  eflogeq  25738  argimlt0  25749  logrec  25894  relogbcxp  25916  atanlogadd  26045  atanlogsub  26047  atantan  26054  ftalem4  26206  ftalem5  26207  basellem3  26213  chtub  26341  dchrpt  26396  dchrsum2  26397  gausslemma2dlem1a  26494  2lgslem3a1  26529  2lgslem3b1  26530  2lgslem3c1  26531  2lgslem3d1  26532  2lgsoddprm  26545  dchrisumlem2  26619  pntrsumbnd2  26696  cnvmot  26883  tglineneq  26986  midexlem  27034  midex  27079  axlowdimlem14  27304  uhgrspansubgrlem  27638  usgrres  27656  usgrnbcnvfv  27713  finsumvtxdg2sstep  27897  uspgr2wlkeq  27993  redwlk  28020  pthdivtx  28076  usgr2wlkspthlem2  28105  wwlknvtx  28189  2wlkdlem6  28275  umgr2wlkon  28294  rusgrnumwwlk  28319  clwwlkwwlksb  28397  clwwlknwwlksnb  28398  clwwnisshclwwsn  28402  clwwlknscsh  28405  clwlknf1oclwwlknlem1  28424  1wlkdlem2  28481  fusgreghash2wsp  28681  2clwwlklem  28686  2clwwlk2clwwlk  28693  numclwwlk6  28733  ofrn2  30956  ofpreima2  30982  wrdsplex  31191  ccatf1  31202  mgcf1o  31260  gsumhashmul  31295  cycpmco2lem5  31376  cycpmco2lem6  31377  cycpmco2lem7  31378  cycpmco2  31379  cyc3co2  31386  imaslmod  31532  rspsnel  31546  elrspunidl  31585  qsidomlem1  31607  qsidomlem2  31608  dimpropd  31671  lbsdiflsp0  31686  extdg1id  31717  zarcmplem  31810  eulerpartlemgvv  32322  pfxwlk  33064  revwlk  33065  pthhashvtx  33068  spthcycl  33070  umgracycusgr  33095  subfacp1lem5  33125  satfvsucsuc  33306  nosupbnd1lem4  33893  noinfbnd2lem1  33912  scutbdaylt  33991  oldlim  34048  madebday  34059  cofcutr  34071  cnambfre  35804  frlmvscadiccat  40217  pwsgprod  40249  evlsval3  40252  evlsbagval  40255  0prjspn  40445  3cubes  40492  gneispace  41697  rr-phpd  41774  grumnudlem  41856  ax6e2ndeqALT  42504  sineq0ALT  42510  fnresdmss  42657  setsv  44782  sprsymrelfolem2  44897  lighneal  45015  isomuspgrlem2c  45234  lincresunit3  45774  2itscp  46079