Theorem simpr1 1195

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpr1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2antr1 1189	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  simpr11  1258  simpr21  1261  simpr31  1264  simp1r1  1270  simp2r1  1276  simp3r1  1282  3anandis  1473  fpr2g  7157  isopolem  7291  fr3nr  7717  sexp3  8095  suppfnss  8131  frrlem4  8231  frrlem8  8235  dif1en  9086  frfi  9185  intrnfi  9319  iinfi  9320  eqsup  9359  fisupcl  9373  cnfcomlem  9608  ttrclss  9629  ackbij1lem15  10143  fpwwe2lem4  10545  dedekindle  11297  ico0  13307  elioc2  13325  elico2  13326  elicc2  13327  iccsplit  13401  fseq1p1m1  13514  elfz0ubfz0  13548  hashtpg  14408  hash7g  14409  swrdsbslen  14588  ccatswrd  14592  wwlktovf1  14880  tanadd  16092  dvds2ln  16216  qredeq  16584  ressress  17174  mreexexlem4d  17570  mreexexd  17571  0catg  17611  2oppccomf  17648  issubc3  17773  fthmon  17853  fuccocl  17891  fucidcl  17892  invfuc  17901  initoeu2lem0  17937  initoeu2lem1  17938  curf2cl  18154  yonedalem4c  18200  yonedalem3  18203  pospo  18266  latjle12  18373  latjlej1  18376  latnlej2  18382  latlem12  18389  latmlem1  18392  latledi  18400  latmlej11  18401  latjass  18406  latj12  18407  latj32  18408  latj13  18409  latj31  18410  latjrot  18411  latjjdi  18414  latjjdir  18415  latdisdlem  18419  prdssgrpd  18658  prdsmndd  18695  imasmnd2  18699  mndissubm  18732  frmdmnd  18784  grpsubrcan  18951  grpsubadd  18958  grpsubsub  18959  grpaddsubass  18960  grpsubsub4  18963  grpnnncan2  18967  imasgrp2  18985  mulgnndir  19033  mulgnn0dir  19034  mulgdir  19036  mulgnnass  19039  mulgnn0ass  19040  mulgass  19041  mulgsubdir  19044  pwsmulg  19049  issubg2  19071  eqgval  19106  qusgrp  19115  kerf1ghm  19176  galcan  19233  gacan  19234  oppgmnd  19283  pmtrprfv  19382  pmtr3ncom  19404  psgnunilem3  19425  cmn32  19729  cmn12  19731  abladdsub  19741  ablsubaddsub  19743  mulgnn0di  19754  mulgdi  19755  mulgsubdi  19758  dprdss  19960  dprdz  19961  dprdf1o  19963  dprdsn  19967  dprd2da  19973  ablfac1b  20001  pgpfac1lem5  20010  prdsrngd  20111  imasrng  20112  srgbinomlem2  20162  srgbinom  20166  ringdilem  20184  prdsringd  20256  imasring  20266  opprrng  20281  mulgass3  20289  dvrass  20344  dvrdir  20348  subrgunit  20523  issubrg2  20525  abvdiv  20762  islss3  20910  prdslmodd  20920  islmhm2  20990  lspsolv  21098  islbs2  21109  islbs3  21110  lbsextlem4  21116  sralmod  21139  ipdir  21594  ipdi  21595  ipsubdir  21597  ipsubdi  21598  ipass  21600  ipassr  21601  ipassr2  21602  ocvlss  21627  sraassaOLD  21825  psrlmod  21915  psrring  21925  psrassa  21928  ply1ass23l  22167  mamudm  22339  matring  22387  matassa  22388  ofco2  22395  mdetunilem1  22556  mdetunilem9  22564  mdetuni0  22565  mdetmul  22567  gsummatr01lem3  22601  iinopn  22846  subbascn  23198  nrmsep2  23300  isnrm3  23303  regsep2  23320  dnsconst  23322  dfconn2  23363  1stcelcls  23405  nllyidm  23433  dislly  23441  upxp  23567  fbasne0  23774  filss  23797  infil  23807  fsubbas  23811  filssufilg  23855  tmdcn2  24033  psmettri  24255  isxmet2d  24271  xmettri  24295  xmetres2  24305  bldisj  24342  blss2ps  24347  blss2  24348  xmstri2  24410  mstri2  24411  xmstri  24412  mstri  24413  xmstri3  24414  mstri3  24415  msrtri  24416  comet  24457  stdbdbl  24461  met2ndci  24466  ngprcan  24554  ngplcan  24555  ngpsubcan  24558  nmtri2  24571  nrgdsdi  24609  nrgdsdir  24610  nlmdsdi  24625  nlmdsdir  24626  blcvx  24742  icccmplem2  24768  pi1grplem  25005  pi1cof  25015  clmpm1dir  25059  cvsdiv  25088  cvsdivcl  25089  cphdivcl  25138  cphsubdir  25164  cphsubdi  25165  cphassr  25168  bcthlem5  25284  rrxcph  25348  volfiniun  25504  volcn  25563  itg1val2  25641  dvconst  25874  dvlip  25954  dvfsumlem4  25992  ftc1a  26000  ulmval  26345  ulmdvlem3  26367  ang180  26780  cvxcl  26951  scvxcvx  26952  sgmmul  27168  logexprlim  27192  dchrabl  27221  nosupbnd1  27682  noinfbnd1lem5  27695  noinfbnd1  27697  sltsss1  27761  motgrp  28615  iscgra1  28882  cgrane1  28884  cgrane2  28885  cgrahl1  28888  cgrahl2  28889  cgracgr  28890  cgratr  28895  cgrabtwn  28898  dfcgra2  28902  sacgr  28903  f1otrge  28944  colinearalglem1  28979  colinearalg  28983  axcgrtr  28988  axlowdimlem16  29030  axeuclidlem  29035  axcontlem7  29043  eengtrkg  29059  eengtrkge  29060  nbfusgrlevtxm2  29451  lfgriswlk  29760  upgrwlkdvde  29810  wwlknbp1  29917  usgrwwlks2on  30031  erclwwlktr  30097  erclwwlkntr  30146  frgr2wwlkeqm  30406  numclwwlk1lem2f  30430  numclwwlk5  30463  friendship  30474  grpodivdiv  30615  grpomuldivass  30616  ablodivdiv4  30629  ablonnncan1  30632  nvmdi  30723  dipassr  30921  archiabllem2c  33277  dvrcan5  33318  rloccring  33352  reofld  33424  eqgvscpbl  33431  qusvsval  33433  quslmod  33439  quslmhm  33440  dvdsruasso2  33467  prmidlc  33529  ssdifidl  33538  ssmxidl  33555  ply1degltlss  33677  r1plmhm  33691  drgextlsp  33750  ccfldsrarelvec  33828  constrconj  33902  constrfin  33903  constrelextdg2  33904  pstmfval  34053  tpr2rico  34069  qqhval2lem  34138  qqhvq  34144  issiga  34269  measdivcst  34381  measdivcstALTV  34382  carsggect  34475  signsply0  34708  tgoldbachgtd  34819  bnj149  35031  bnj1118  35140  bnj1128  35146  erdszelem9  35393  resconn  35440  cvmseu  35470  cvmlift2lem12  35508  ex-sategoelel  35615  elmrsubrn  35714  mclsind  35764  r1peuqusdeg1  35837  cgrid2  36197  segconeu  36205  btwncomim  36207  btwnswapid  36211  cgrxfr  36249  btwnxfr  36250  colineardim1  36255  brofs2  36271  brifs2  36272  idinside  36278  endofsegid  36279  btwnconn1lem7  36287  btwnconn1lem11  36291  btwnconn1  36295  segcon2  36299  seglemin  36307  segletr  36308  btwnsegle  36311  colinbtwnle  36312  broutsideof2  36316  broutsideof3  36320  outsidele  36326  fvray  36335  fvline  36338  linerflx1  36343  ellines  36346  ivthALT  36529  weiunpo  36659  poimirlem32  37849  ftc1anc  37898  sdclem1  37940  sstotbnd2  37971  zerdivemp1x  38144  isdrngo2  38155  iscringd  38195  lsmsat  39264  lfladdcl  39327  lflnegcl  39331  lflvscl  39333  lshpkrlem4  39369  lshpkrlem6  39371  ldualgrplem  39401  lduallmodlem  39408  latmassOLD  39485  latm12  39486  latm32  39487  latmrot  39488  latmmdiN  39490  latmmdir  39491  omlfh1N  39514  omlfh3N  39515  cvlexchb1  39586  cvlexch3  39588  cvlexch4N  39589  cvlatexchb1  39590  cvlsupr2  39599  hlatjass  39626  hlatj12  39627  hlatj32  39628  cvratlem  39677  cvrat  39678  atcvrj0  39684  cvrat2  39685  atltcvr  39691  atexchltN  39697  cvrat3  39698  cvrat4  39699  3dimlem3  39717  3dimlem3OLDN  39718  3at  39746  2atneat  39771  llncmp  39778  2at0mat0  39781  2atmat0  39782  lplnnle2at  39797  llncvrlpln  39814  lplncmp  39818  lplnexllnN  39820  2llnjaN  39822  4atlem11  39865  lplncvrlvol  39872  lvolcmp  39873  2atm2atN  40041  elpaddatriN  40059  paddasslem9  40084  paddass  40094  padd12N  40095  paddssw2  40100  paddss  40101  pmodlem2  40103  pmodN  40106  pmapjlln1  40111  atmod1i1  40113  atmod1i2  40115  pexmidlem2N  40227  pexmidlem6N  40231  pl42N  40239  lhpm0atN  40285  lautlt  40347  lautcvr  40348  lautj  40349  lautm  40350  ltrneq2  40404  cdlemc3  40449  cdlemc4  40450  cdlemd1  40454  cdleme1b  40482  cdleme1  40483  cdleme2  40484  cdleme3e  40488  cdlemefr27cl  40659  cdlemefs27cl  40669  cdleme42mN  40743  cdlemftr2  40822  trljco  40996  tgrpgrplem  41005  tendoplass  41039  tendodi1  41040  tendodi2  41041  cdlemk36  41169  erngdvlem3  41246  erngdvlem3-rN  41254  tendospdi1  41276  dvalveclem  41281  dialss  41302  dvhvaddass  41353  dvhopvsca  41358  dvhlveclem  41364  diblss  41426  diclss  41449  dihmeetlem12N  41574  dihmeetlem15N  41577  dihmeetlem16N  41578  dihmeetlem17N  41579  dihmeetlem18N  41580  dihmeetlem19N  41581  dvh4dimN  41703  lpolvN  41742  lclkr  41789  lclkrs  41795  lcfr  41841  aks6d1c1  42366  irrapxlem6  43065  jm2.26lem3  43239  dgrsub2  43373  mpaadgr  43392  mendring  43426  mendlmod  43427  mendassa  43428  nnoeomeqom  43550  omabs2  43570  relexpmulg  43947  iunrelexpmin2  43949  relexpxpmin  43954  neicvgel1  44356  fmuldfeq  45825  stoweidlem43  46283  stoweidlem52  46292  stoweidlem53  46293  stoweidlem56  46296  stoweidlem57  46297  issmfle  46985  issmfgt  46996  issmfge  47010  submodaddmod  47583  fmtnoprmfac1  47807  fmtnoprmfac2  47809  clnbgredg  48082  cycl3grtrilem  48188  grlimprclnbgr  48238  grlimprclnbgredg  48239  upgrwlkupwlk  48382  copissgrp  48410  cznrng  48503  funcringcsetcALTV2lem9  48540  funcringcsetclem9ALTV  48563  linccl  48656  lincext1  48696  lincext3  48698  lincresunit2  48720  line  48974  rrxline  48976  itsclc0yqsol  49006  resipos  49216  topdlat  49245  catprs  49252  endmndlem  49256  idmon  49261  idepi  49262  thincmon  49674  thincepi  49675  grptcmon  49834  grptcepi  49835