Theorem simpr1 1213

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 490	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2antr1 1207	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr11  1276  simpr21  1279  simpr31  1282  simp1r1  1288  simp2r1  1294  simp3r1  1300  3anandis  1500  fpr2g  7214  isopolem  7350  fr3nr  7775  sexp3  8155  suppfnss  8191  frrlem4  8292  frrlem8  8296  dif1en  9160  frfi  9259  intrnfi  9390  iinfi  9391  eqsup  9430  fisupcl  9444  cnfcomlem  9682  ttrclss  9703  ackbij1lem15  10239  fpwwe2lem4  10647  dedekindle  11402  ico0  13448  elioc2  13466  elico2  13467  elicc2  13468  iccsplit  13542  fseq1p1m1  13657  elfz0ubfz0  13691  hashtpg  14554  hash7g  14555  swrdsbslen  14738  ccatswrd  14742  wwlktovf1  15034  tanadd  16261  dvds2ln  16385  qredeq  16753  ressress  17345  mreexexlem4d  17741  mreexexd  17742  0catg  17782  2oppccomf  17819  issubc3  17944  fthmon  18024  fuccocl  18062  fucidcl  18063  invfuc  18072  initoeu2lem0  18108  initoeu2lem1  18109  curf2cl  18325  yonedalem4c  18371  yonedalem3  18374  pospo  18437  latjle12  18544  latjlej1  18547  latnlej2  18553  latlem12  18560  latmlem1  18563  latledi  18571  latmlej11  18572  latjass  18577  latj12  18578  latj32  18579  latj13  18580  latj31  18581  latjrot  18582  latjjdi  18585  latjjdir  18586  latdisdlem  18590  prdssgrpd  18841  prdsmndd  18883  imasmnd2  18887  mndissubm  18921  frmdmnd  18974  grpsubrcan  19150  grpsubadd  19157  grpsubsub  19158  grpaddsubass  19159  grpsubsub4  19162  grpnnncan2  19166  imasgrp2  19184  mulgnndir  19232  mulgnn0dir  19233  mulgdir  19235  mulgnnass  19238  mulgnn0ass  19239  mulgass  19240  mulgsubdir  19243  pwsmulg  19248  issubg2  19271  eqgval  19308  qusgrp  19320  kerf1ghm  19380  galcan  19437  gacan  19438  oppgmnd  19487  pmtrprfv  19586  pmtr3ncom  19608  psgnunilem3  19629  cmn32  19933  cmn12  19935  abladdsub  19945  ablsubaddsub  19947  mulgnn0di  19958  mulgdi  19959  mulgsubdi  19962  dprdss  20164  dprdz  20165  dprdf1o  20167  dprdsn  20171  dprd2da  20177  ablfac1b  20205  pgpfac1lem5  20214  prdsrngd  20317  imasrng  20318  srgbinomlem2  20372  srgbinom  20376  ringdilem  20394  prdsringd  20467  imasring  20477  opprrng  20492  mulgass3  20500  dvrass  20555  dvrdir  20559  subrgunit  20758  issubrg2  20760  abvdiv  21001  islss3  21149  prdslmodd  21159  islmhm2  21228  lspsolv  21336  islbs2  21347  islbs3  21348  lbsextlem4  21354  sralmod  21377  prmidlc  21542  ssdifidl  21554  ipdir  21858  ipdi  21859  ipsubdir  21861  ipsubdi  21862  ipass  21864  ipassr  21865  ipassr2  21866  ocvlss  21891  psrlmod  22180  psrring  22190  psrassa  22193  ply1ass23l  22457  mamudm  22623  matring  22671  matassa  22672  ofco2  22679  mdetunilem1  22840  mdetunilem9  22848  mdetuni0  22849  mdetmul  22851  gsummatr01lem3  22885  iinopn  23133  subbascn  23485  nrmsep2  23587  isnrm3  23590  regsep2  23607  dnsconst  23609  dfconn2  23650  1stcelcls  23693  nllyidm  23721  dislly  23729  upxp  23855  fbasne0  24062  filss  24085  infil  24095  fsubbas  24099  filssufilg  24143  tmdcn2  24321  psmettri  24543  isxmet2d  24559  xmettri  24583  xmetres2  24593  bldisj  24630  blss2ps  24635  blss2  24636  xmstri2  24698  mstri2  24699  xmstri  24700  mstri  24701  xmstri3  24702  mstri3  24703  msrtri  24704  comet  24745  stdbdbl  24749  met2ndci  24754  ngprcan  24842  ngplcan  24843  ngpsubcan  24846  nmtri2  24859  nrgdsdi  24897  nrgdsdir  24898  nlmdsdi  24913  nlmdsdir  24914  blcvx  25030  icccmplem2  25056  pi1grplem  25283  pi1cof  25293  clmpm1dir  25337  cvsdiv  25366  cvsdivcl  25367  cphdivcl  25416  cphsubdir  25442  cphsubdi  25443  cphassr  25446  bcthlem5  25562  rrxcph  25626  volfiniun  25781  volcn  25840  itg1val2  25918  dvconst  26151  dvlip  26227  dvfsumlem4  26263  ftc1a  26271  ulmval  26623  ulmdvlem3  26645  ang180  27059  cvxcl  27229  scvxcvx  27230  sgmmul  27445  logexprlim  27469  dchrabl  27498  nosupbnd1  27958  noinfbnd1lem5  27971  noinfbnd1  27973  sltsss1  28038  motgrp  28893  iscgra1  29204  cgrane1  29206  cgrane2  29207  cgrahl1  29210  cgrahl2  29211  cgracgr  29212  cgratr  29217  cgrabtwn  29221  dfcgra2  29225  sacgr  29226  angmgmaddcl  29278  f1otrge  29336  colinearalglem1  29371  colinearalg  29375  axcgrtr  29380  axlowdimlem16  29422  axeuclidlem  29427  axcontlem7  29435  eengtrkg  29451  eengtrkge  29452  nbfusgrlevtxm2  29846  lfgriswlk  30158  upgrwlkdvde  30210  wwlknbp1  30320  usgrwwlks2on  30434  erclwwlktr  30500  erclwwlkntr  30549  frgr2wwlkeqm  30819  numclwwlk1lem2f  30843  numclwwlk5  30876  friendship  30887  grpodivdiv  31029  grpomuldivass  31030  ablodivdiv4  31043  ablonnncan1  31046  nvmdi  31137  dipassr  31335  archiabllem2c  33643  dvrcan5  33683  rloccring  33719  reofld  33791  eqgvscpbl  33798  qusvsval  33800  quslmod  33806  quslmhm  33807  dvdsruasso2  33827  ssmxidl  33885  ply1degltlss  34014  r1plmhm  34027  drgextlsp  34112  ccfldsrarelvec  34189  constrconj  34263  constrfin  34264  constrelextdg2  34265  pstmfval  34414  tpr2rico  34430  qqhval2lem  34499  qqhvq  34505  issiga  34630  measdivcst  34743  measdivcstALTV  34744  carsggect  34837  signsply0  35067  tgoldbachgtd  35178  bnj149  35392  bnj1118  35501  bnj1128  35507  erdszelem9  35786  resconn  35833  cvmseu  35863  cvmlift2lem12  35901  ex-sategoelel  36008  elmrsubrn  36107  mclsind  36157  r1peuqusdeg1  36230  cgrid2  36591  segconeu  36599  btwncomim  36601  btwnswapid  36605  cgrxfr  36643  btwnxfr  36644  colineardim1  36649  brofs2  36665  brifs2  36666  idinside  36672  endofsegid  36673  btwnconn1lem7  36681  btwnconn1lem11  36685  btwnconn1  36689  segcon2  36693  seglemin  36701  segletr  36702  btwnsegle  36705  colinbtwnle  36706  broutsideof2  36710  broutsideof3  36714  outsidele  36720  fvray  36729  fvline  36732  linerflx1  36737  ellines  36740  ivthALT  36962  weiunpo  37092  poimirlem32  38409  ftc1anc  38458  sdclem1  38501  sstotbnd2  38532  zerdivemp1x  38705  isdrngo2  38716  iscringd  38756  lsmsat  39889  lfladdcl  39952  lflnegcl  39956  lflvscl  39958  lshpkrlem4  39994  lshpkrlem6  39996  ldualgrplem  40026  lduallmodlem  40033  latmassOLD  40110  latm12  40111  latm32  40112  latmrot  40113  latmmdiN  40115  latmmdir  40116  omlfh1N  40139  omlfh3N  40140  cvlexchb1  40211  cvlexch3  40213  cvlexch4N  40214  cvlatexchb1  40215  cvlsupr2  40224  hlatjass  40251  hlatj12  40252  hlatj32  40253  cvratlem  40302  cvrat  40303  atcvrj0  40309  cvrat2  40310  atltcvr  40316  atexchltN  40322  cvrat3  40323  cvrat4  40324  3dimlem3  40342  3dimlem3OLDN  40343  3at  40371  2atneat  40396  llncmp  40403  2at0mat0  40406  2atmat0  40407  lplnnle2at  40422  llncvrlpln  40439  lplncmp  40443  lplnexllnN  40445  2llnjaN  40447  4atlem11  40490  lplncvrlvol  40497  lvolcmp  40498  2atm2atN  40666  elpaddatriN  40684  paddasslem9  40709  paddass  40719  padd12N  40720  paddssw2  40725  paddss  40726  pmodlem2  40728  pmodN  40731  pmapjlln1  40736  atmod1i1  40738  atmod1i2  40740  pexmidlem2N  40852  pexmidlem6N  40856  pl42N  40864  lhpm0atN  40910  lautlt  40972  lautcvr  40973  lautj  40974  lautm  40975  ltrneq2  41029  cdlemc3  41074  cdlemc4  41075  cdlemd1  41079  cdleme1b  41107  cdleme1  41108  cdleme2  41109  cdleme3e  41113  cdlemefr27cl  41284  cdlemefs27cl  41294  cdleme42mN  41368  cdlemftr2  41447  trljco  41621  tgrpgrplem  41630  tendoplass  41664  tendodi1  41665  tendodi2  41666  cdlemk36  41794  erngdvlem3  41871  erngdvlem3-rN  41879  tendospdi1  41901  dvalveclem  41906  dialss  41927  dvhvaddass  41978  dvhopvsca  41983  dvhlveclem  41989  diblss  42051  diclss  42074  dihmeetlem12N  42199  dihmeetlem15N  42202  dihmeetlem16N  42203  dihmeetlem17N  42204  dihmeetlem18N  42205  dihmeetlem19N  42206  dvh4dimN  42328  lpolvN  42367  lclkr  42414  lclkrs  42420  lcfr  42466  aks6d1c1  42990  irrapxlem6  43676  jm2.26lem3  43850  dgrsub2  43984  mpaadgr  44003  mendring  44037  mendlmod  44038  mendassa  44039  nnoeomeqom  44161  omabs2  44181  relexpmulg  44558  iunrelexpmin2  44560  relexpxpmin  44565  neicvgel1  44967  fmuldfeq  46421  stoweidlem43  46879  stoweidlem52  46888  stoweidlem53  46889  stoweidlem56  46892  stoweidlem57  46893  issmfle  47581  issmfgt  47592  issmfge  47606  submodaddmod  48243  fmtnoprmfac1  48476  fmtnoprmfac2  48478  clnbgredg  48764  cycl3grtrilem  48870  grlimprclnbgr  48920  grlimprclnbgredg  48921  upgrwlkupwlk  49064  copissgrp  49091  cznrng  49184  funcringcsetcALTV2lem9  49221  funcringcsetclem9ALTV  49244  idomcanl  49270  linccl  49352  lincext1  49392  lincext3  49394  lincresunit2  49416  line  49670  rrxline  49672  itsclc0yqsol  49702  resipos  49909  topdlat  49938  catprs  49945  endmndlem  49949  idmon  49954  idepi  49955  thincmon  50367  thincepi  50368  grptcmon  50527  grptcepi  50528  nellindf  50811