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  5104  axprlem4OLD  5384  brcogw  5832  funfni  6624  f1un  6820  fvelimab  6933  dff3  7072  fnex  7191  ralima  7211  f1cofveqaeq  7232  f1eqcocnv  7276  caofid0l  7686  caofid0r  7687  caofid1  7688  caofid2  7689  onmindif2  7783  limsssuc  7826  mptcnfimad  7965  fnse  8112  frrlem13  8277  iinon  8309  smoord  8334  smoword  8335  tfrlem11  8356  coflton  8635  cofonr  8638  naddasslem2  8659  boxcutc  8914  f1domg  8943  phpeqd  9176  ominf  9205  f1finf1o  9216  findcard3OLD  9230  unfilem1  9254  f1opwfi  9307  marypha2  9390  supmax  9419  infmin  9447  ordtypelem6  9476  oiexg  9488  oien  9491  cantnff  9627  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  ttrcltr  9669  ttrclselem2  9679  opwf  9765  rankopb  9805  xpnum  9904  infxpenlem  9966  infxp  10167  cflim2  10216  cofsmo  10222  cfsmolem  10223  cfcoflem  10225  ssfin3ds  10283  isf34lem5  10331  isf34lem6  10333  isfin1-3  10339  axcc3  10391  alephval2  10525  fpwwe2lem7  10590  canthp1  10607  tsken  10707  ltaddpr  10987  dedekind  11337  recextlem2  11809  recex  11810  gt0div  12049  ge0div  12050  lerec2  12071  uzwo2  12871  infssuzcl  12891  qmulcl  12926  xnegdi  13208  xmulpnf1n  13238  xadddi2  13257  fzm1  13568  2submod  13897  addmodlteq  13911  expnlbnd  14198  faclbnd5  14263  hasheni  14313  hashdifpr  14380  hashgt23el  14389  ccatrn  14554  ccatalpha  14558  swrds1  14631  swrdccat2  14634  ccatpfx  14666  swrdccatin2  14694  pfxccatin12lem2  14696  revccat  14731  revrev  14732  swrdco  14803  relexpindlem  15029  resqrex  15216  fzomaxdiflem  15309  climconst  15509  serf0  15647  fsumf1o  15689  fsumrev  15745  fsumabs  15767  cvgcmp  15782  binomlem  15795  isumshft  15805  climcndslem1  15815  climcndslem2  15816  climcnds  15817  supcvg  15822  fprodcl2lem  15916  tanneg  16116  rpnnen2lem11  16192  modm1div  16234  fzo0dvdseq  16293  bitsfzolem  16404  gcdcllem3  16471  hashdvds  16745  prmdivdiv  16757  reumodprminv  16775  nnnn0modprm0  16777  pythagtrip  16805  dvdsprmpweqle  16857  pockthg  16877  4sqlem9  16917  vdwmc2  16950  vdwlem2  16953  imasaddflem  17493  acsfn1  17622  acsfn1c  17623  acsfn2  17624  oppccofval  17677  rescabs  17795  diag2  18206  grpinvalem  18600  issubmnd  18688  imasmnd  18702  pwsco2mhm  18760  gsumwspan  18773  frmdss2  18790  grpinvssd  18949  pwssub  18986  imasgrp  18988  subginv  19065  subginvcl  19067  ecqusaddcl  19125  ghmpreima  19170  conjnsg  19186  gass  19233  gsmsymgreqlem2  19361  f1omvdmvd  19373  symgsssg  19397  symgfisg  19398  symgtrinv  19402  psgnunilem5  19424  sylow1lem2  19529  odcau  19534  sylow2a  19549  sylow2  19556  efgsp1  19667  frgpuptf  19700  frgpuptinv  19701  frgpupf  19703  frgpup3lem  19707  mulgdi  19756  gsumval3eu  19834  gsumzsplit  19857  gsumzmhm  19867  gsumxp2  19910  prdsgsum  19911  fsfnn0gsumfsffz  19913  ablfaclem3  20019  srgbinomlem  20139  gsummgp0  20227  imasring  20239  dvdsr01  20280  rngisom1  20375  01eq0ring  20439  issubrng2  20467  subrgcrng  20484  subrginv  20497  isdrngd  20674  imadrhmcl  20706  abv1z  20733  lcomfsupp  20808  lmodvneg1  20811  lspsn  20908  lmhmco  20950  lmhmima  20954  lmhmpreima  20955  reslmhm  20959  lbsextlem2  21069  isridlrng  21129  lidl0cl  21130  elrspsn  21150  rnglidlmmgm  21155  rnglidlmsgrp  21156  2idlcpblrng  21181  quscrng  21193  rngqiprngghmlem1  21197  rngqiprngghmlem3  21199  rngqiprnglinlem3  21203  rngqiprngimf1lem  21204  rngqiprngimf  21207  rng2idl1cntr  21215  znfld  21470  ipassr2  21556  ocvin  21583  pjfo  21624  obsne0  21634  frlmgsum  21681  aspval2  21807  psrlinv  21864  mplsubglem  21908  mpllsslem  21909  evlslem4  21983  evlslem1  21989  mpfind  22014  evls1rhm  22209  madetsumid  22348  scmatcrng  22408  mdetleib2  22475  cramerimplem1  22570  m2pmfzgsumcl  22635  decpmatmul  22659  pmatcollpwscmat  22678  idpm2idmp  22688  pm2mpmhmlem1  22705  chpscmatgsummon  22732  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  topbas  22859  uncld  22928  incld  22930  elcls  22960  neiptopnei  23019  resttopon  23048  restdis  23065  cnclima  23155  paste  23181  cncmp  23279  clsconn  23317  conncompcld  23321  1stcfb  23332  2ndcsb  23336  2ndcredom  23337  kgencmp2  23433  txss12  23492  qtoptop2  23586  qtoptopon  23591  hmphindis  23684  uffixfr  23810  ufildr  23818  isfcls2  23900  tgplacthmeo  23990  tsmsgsum  24026  tgptsmscld  24038  tsmssplit  24039  ustuqtop5  24133  uspreg  24161  prdsxmetlem  24256  prdsbl  24379  metss  24396  metrest  24412  nrmmetd  24462  isngp2  24485  ngpsubcan  24502  lssnlm  24589  nmoid  24630  opnreen  24720  mpomulcn  24758  evth  24858  htpyco2  24878  phtpyco2  24889  clmvz  25011  tcphcph  25137  iscmet3  25193  metcld  25206  bcthlem2  25225  cssbn  25275  chlcsschl  25278  minveclem1  25324  evthicc2  25361  ovolunlem1a  25397  ovolicc2lem1  25418  ovolicc2lem4  25421  ovolicc2lem5  25422  uniioombllem2  25484  uniioombllem3  25486  vitalilem2  25510  vitalilem4  25512  vitalilem5  25513  itg2monolem1  25651  cpnres  25839  rolle  25894  dvlip2  25900  dvivthlem2  25914  dvfsumrlimge0  25937  deg1pwle  26025  plydivlem4  26204  ulm0  26300  efif1olem1  26451  efif1olem2  26452  eflogeq  26511  argimlt0  26522  logrec  26673  relogbcxp  26695  atanlogadd  26824  atanlogsub  26826  atantan  26833  ftalem4  26986  ftalem5  26987  basellem3  26993  chtub  27123  dchrpt  27178  dchrsum2  27179  gausslemma2dlem1a  27276  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  2lgsoddprm  27327  dchrisumlem2  27401  pntrsumbnd2  27478  nosupbnd1lem4  27623  noinfbnd2lem1  27642  scutbdaylt  27730  oldlim  27798  madebday  27811  cofcutr  27832  addsbday  27924  negsbdaylem  27962  absmuls  28146  abssneg  28149  cnvmot  28468  tglineneq  28571  midexlem  28619  midex  28664  axlowdimlem14  28882  uhgrspansubgrlem  29217  usgrres  29235  usgrnbcnvfv  29292  finsumvtxdg2sstep  29477  uspgr2wlkeq  29574  redwlk  29600  pthdivtx  29657  usgr2wlkspthlem2  29688  wwlknvtx  29775  2wlkdlem6  29861  umgr2wlkon  29880  rusgrnumwwlk  29905  clwwlkwwlksb  29983  clwwlknwwlksnb  29984  clwwnisshclwwsn  29988  clwwlknscsh  29991  clwlknf1oclwwlknlem1  30010  1wlkdlem2  30067  fusgreghash2wsp  30267  2clwwlklem  30272  2clwwlk2clwwlk  30279  numclwwlk6  30319  prssad  32458  prssbd  32459  ofrn2  32564  ofpreima2  32590  sgnval2  32658  argcj  32672  wrdsplex  32857  ccatf1  32870  mgcf1o  32929  gsumfs2d  32995  gsumhashmul  33001  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cyc3co2  33097  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnsubrunlem1  33198  erler  33216  fracerl  33256  imaslmod  33324  elrspunidl  33399  qsidomlem1  33423  qsidomlem2  33424  ssdifidllem  33427  ssdifidlprm  33429  ressply1evls1  33534  exsslsb  33592  dimpropd  33604  lbsdiflsp0  33622  extdg1id  33661  madjusmdetlem2  33818  zarcmplem  33871  eulerpartlemgvv  34367  boolesineq  34446  vonf1owev  35095  pfxwlk  35111  revwlk  35112  pthhashvtx  35115  spthcycl  35116  umgracycusgr  35141  subfacp1lem5  35171  satfvsucsuc  35352  ply1divalg3  35629  weiunfrlem  36452  cnambfre  37662  frlmvscadiccat  42494  ricdrng1  42516  pwsgprod  42532  evlsval3  42547  evlsbagval  42554  0prjspn  42616  3cubes  42678  oninfint  43225  onexomgt  43230  onexoegt  43233  ordeldif  43247  oacl2g  43319  onmcl  43320  omabs2  43321  omcl2  43322  tfsconcatfv  43330  tfsconcatrev  43337  ofoafg  43343  ofoafo  43345  ofoaass  43349  ofoacom  43350  onsucunifi  43359  oaun3lem1  43363  oadif1lem  43368  oadif1  43369  naddwordnexlem4  43390  safesnsupfilb  43407  gneispace  44123  rr-phpd  44198  grumnudlem  44274  ax6e2ndeqALT  44920  sineq0ALT  44926  fnresdmss  45162  saliinclf  46324  setsv  47379  sprsymrelfolem2  47494  lighneal  47612  grimuhgr  47887  grimcnv  47888  uhgrimedgi  47890  uhgrimedg  47891  isuspgrim0lem  47893  isuspgrim0  47894  upgrimtrlslem1  47904  upgrimtrlslem2  47905  clnbgrgrim  47934  grimedg  47935  isubgr3stgrlem8  47972  clnbgr3stgrgrlic  48011  lincresunit3  48470  2itscp  48770  resccat  49063