Theorem simpr1 1207

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simpr11  1270  simpr21  1273  simpr31  1276  simp1r1  1282  simp2r1  1288  simp3r1  1294  3anandis  1491  fpr2g  7191  isopolem  7325  fr3nr  7751  sexp3  8128  suppfnss  8164  frrlem4  8265  frrlem8  8269  dif1en  9126  frfi  9225  intrnfi  9359  iinfi  9360  eqsup  9399  fisupcl  9413  cnfcomlem  9651  ttrclss  9672  ackbij1lem15  10186  fpwwe2lem4  10589  dedekindle  11344  ico0  13392  elioc2  13410  elico2  13411  elicc2  13412  iccsplit  13486  fseq1p1m1  13600  elfz0ubfz0  13634  hashtpg  14495  hash7g  14496  swrdsbslen  14675  ccatswrd  14679  wwlktovf1  14967  tanadd  16182  dvds2ln  16306  qredeq  16674  ressress  17266  mreexexlem4d  17662  mreexexd  17663  0catg  17703  2oppccomf  17740  issubc3  17865  fthmon  17945  fuccocl  17983  fucidcl  17984  invfuc  17993  initoeu2lem0  18029  initoeu2lem1  18030  curf2cl  18246  yonedalem4c  18292  yonedalem3  18295  pospo  18358  latjle12  18465  latjlej1  18468  latnlej2  18474  latlem12  18481  latmlem1  18484  latledi  18492  latmlej11  18493  latjass  18498  latj12  18499  latj32  18500  latj13  18501  latj31  18502  latjrot  18503  latjjdi  18506  latjjdir  18507  latdisdlem  18511  prdssgrpd  18750  prdsmndd  18787  imasmnd2  18791  mndissubm  18824  frmdmnd  18876  grpsubrcan  19046  grpsubadd  19053  grpsubsub  19054  grpaddsubass  19055  grpsubsub4  19058  grpnnncan2  19062  imasgrp2  19080  mulgnndir  19128  mulgnn0dir  19129  mulgdir  19131  mulgnnass  19134  mulgnn0ass  19135  mulgass  19136  mulgsubdir  19139  pwsmulg  19144  issubg2  19166  eqgval  19201  qusgrp  19210  kerf1ghm  19270  galcan  19327  gacan  19328  oppgmnd  19377  pmtrprfv  19476  pmtr3ncom  19498  psgnunilem3  19519  cmn32  19823  cmn12  19825  abladdsub  19835  ablsubaddsub  19837  mulgnn0di  19848  mulgdi  19849  mulgsubdi  19852  dprdss  20054  dprdz  20055  dprdf1o  20057  dprdsn  20061  dprd2da  20067  ablfac1b  20095  pgpfac1lem5  20104  prdsrngd  20205  imasrng  20206  srgbinomlem2  20256  srgbinom  20260  ringdilem  20278  prdsringd  20348  imasring  20358  opprrng  20373  mulgass3  20381  dvrass  20436  dvrdir  20440  subrgunit  20619  issubrg2  20621  abvdiv  20858  islss3  21006  prdslmodd  21016  islmhm2  21085  lspsolv  21193  islbs2  21204  islbs3  21205  lbsextlem4  21211  sralmod  21234  ipdir  21671  ipdi  21672  ipsubdir  21674  ipsubdi  21675  ipass  21677  ipassr  21678  ipassr2  21679  ocvlss  21704  psrlmod  21991  psrring  22001  psrassa  22004  ply1ass23l  22268  mamudm  22435  matring  22483  matassa  22484  ofco2  22491  mdetunilem1  22652  mdetunilem9  22660  mdetuni0  22661  mdetmul  22663  gsummatr01lem3  22697  iinopn  22942  subbascn  23294  nrmsep2  23396  isnrm3  23399  regsep2  23416  dnsconst  23418  dfconn2  23459  1stcelcls  23501  nllyidm  23529  dislly  23537  upxp  23663  fbasne0  23870  filss  23893  infil  23903  fsubbas  23907  filssufilg  23951  tmdcn2  24129  psmettri  24351  isxmet2d  24367  xmettri  24391  xmetres2  24401  bldisj  24438  blss2ps  24443  blss2  24444  xmstri2  24506  mstri2  24507  xmstri  24508  mstri  24509  xmstri3  24510  mstri3  24511  msrtri  24512  comet  24553  stdbdbl  24557  met2ndci  24562  ngprcan  24650  ngplcan  24651  ngpsubcan  24654  nmtri2  24667  nrgdsdi  24705  nrgdsdir  24706  nlmdsdi  24721  nlmdsdir  24722  blcvx  24838  icccmplem2  24864  pi1grplem  25091  pi1cof  25101  clmpm1dir  25145  cvsdiv  25174  cvsdivcl  25175  cphdivcl  25224  cphsubdir  25250  cphsubdi  25251  cphassr  25254  bcthlem5  25370  rrxcph  25434  volfiniun  25589  volcn  25648  itg1val2  25726  dvconst  25959  dvlip  26035  dvfsumlem4  26071  ftc1a  26079  ulmval  26420  ulmdvlem3  26442  ang180  26856  cvxcl  27026  scvxcvx  27027  sgmmul  27242  logexprlim  27266  dchrabl  27295  nosupbnd1  27755  noinfbnd1lem5  27768  noinfbnd1  27770  sltsss1  27835  motgrp  28689  iscgra1  28956  cgrane1  28958  cgrane2  28959  cgrahl1  28962  cgrahl2  28963  cgracgr  28964  cgratr  28969  cgrabtwn  28972  dfcgra2  28976  sacgr  28977  f1otrge  29018  colinearalglem1  29053  colinearalg  29057  axcgrtr  29062  axlowdimlem16  29104  axeuclidlem  29109  axcontlem7  29117  eengtrkg  29133  eengtrkge  29134  nbfusgrlevtxm2  29525  lfgriswlk  29833  upgrwlkdvde  29883  wwlknbp1  29990  usgrwwlks2on  30104  erclwwlktr  30170  erclwwlkntr  30219  frgr2wwlkeqm  30479  numclwwlk1lem2f  30503  numclwwlk5  30536  friendship  30547  grpodivdiv  30689  grpomuldivass  30690  ablodivdiv4  30703  ablonnncan1  30706  nvmdi  30797  dipassr  30995  archiabllem2c  33336  dvrcan5  33377  rloccring  33413  reofld  33490  eqgvscpbl  33497  qusvsval  33499  quslmod  33505  quslmhm  33506  dvdsruasso2  33533  prmidlc  33595  ssdifidl  33605  ssmxidl  33623  ply1degltlss  33753  r1plmhm  33767  drgextlsp  33852  ccfldsrarelvec  33929  constrconj  34003  constrfin  34004  constrelextdg2  34005  pstmfval  34154  tpr2rico  34170  qqhval2lem  34239  qqhvq  34245  issiga  34370  measdivcst  34482  measdivcstALTV  34483  carsggect  34576  signsply0  34809  tgoldbachgtd  34920  bnj149  35134  bnj1118  35243  bnj1128  35249  erdszelem9  35513  resconn  35560  cvmseu  35590  cvmlift2lem12  35628  ex-sategoelel  35735  elmrsubrn  35834  mclsind  35884  r1peuqusdeg1  35957  cgrid2  36317  segconeu  36325  btwncomim  36327  btwnswapid  36331  cgrxfr  36369  btwnxfr  36370  colineardim1  36375  brofs2  36391  brifs2  36392  idinside  36398  endofsegid  36399  btwnconn1lem7  36407  btwnconn1lem11  36411  btwnconn1  36415  segcon2  36419  seglemin  36427  segletr  36428  btwnsegle  36431  colinbtwnle  36432  broutsideof2  36436  broutsideof3  36440  outsidele  36446  fvray  36455  fvline  36458  linerflx1  36463  ellines  36466  ivthALT  36659  weiunpo  36789  poimirlem32  38115  ftc1anc  38164  sdclem1  38206  sstotbnd2  38237  zerdivemp1x  38410  isdrngo2  38421  iscringd  38461  lsmsat  39596  lfladdcl  39659  lflnegcl  39663  lflvscl  39665  lshpkrlem4  39701  lshpkrlem6  39703  ldualgrplem  39733  lduallmodlem  39740  latmassOLD  39817  latm12  39818  latm32  39819  latmrot  39820  latmmdiN  39822  latmmdir  39823  omlfh1N  39846  omlfh3N  39847  cvlexchb1  39918  cvlexch3  39920  cvlexch4N  39921  cvlatexchb1  39922  cvlsupr2  39931  hlatjass  39958  hlatj12  39959  hlatj32  39960  cvratlem  40009  cvrat  40010  atcvrj0  40016  cvrat2  40017  atltcvr  40023  atexchltN  40029  cvrat3  40030  cvrat4  40031  3dimlem3  40049  3dimlem3OLDN  40050  3at  40078  2atneat  40103  llncmp  40110  2at0mat0  40113  2atmat0  40114  lplnnle2at  40129  llncvrlpln  40146  lplncmp  40150  lplnexllnN  40152  2llnjaN  40154  4atlem11  40197  lplncvrlvol  40204  lvolcmp  40205  2atm2atN  40373  elpaddatriN  40391  paddasslem9  40416  paddass  40426  padd12N  40427  paddssw2  40432  paddss  40433  pmodlem2  40435  pmodN  40438  pmapjlln1  40443  atmod1i1  40445  atmod1i2  40447  pexmidlem2N  40559  pexmidlem6N  40563  pl42N  40571  lhpm0atN  40617  lautlt  40679  lautcvr  40680  lautj  40681  lautm  40682  ltrneq2  40736  cdlemc3  40781  cdlemc4  40782  cdlemd1  40786  cdleme1b  40814  cdleme1  40815  cdleme2  40816  cdleme3e  40820  cdlemefr27cl  40991  cdlemefs27cl  41001  cdleme42mN  41075  cdlemftr2  41154  trljco  41328  tgrpgrplem  41337  tendoplass  41371  tendodi1  41372  tendodi2  41373  cdlemk36  41501  erngdvlem3  41578  erngdvlem3-rN  41586  tendospdi1  41608  dvalveclem  41613  dialss  41634  dvhvaddass  41685  dvhopvsca  41690  dvhlveclem  41696  diblss  41758  diclss  41781  dihmeetlem12N  41906  dihmeetlem15N  41909  dihmeetlem16N  41910  dihmeetlem17N  41911  dihmeetlem18N  41912  dihmeetlem19N  41913  dvh4dimN  42035  lpolvN  42074  lclkr  42121  lclkrs  42127  lcfr  42173  aks6d1c1  42697  irrapxlem6  43368  jm2.26lem3  43542  dgrsub2  43676  mpaadgr  43695  mendring  43729  mendlmod  43730  mendassa  43731  nnoeomeqom  43853  omabs2  43873  relexpmulg  44250  iunrelexpmin2  44252  relexpxpmin  44257  neicvgel1  44659  fmuldfeq  46123  stoweidlem43  46581  stoweidlem52  46590  stoweidlem53  46591  stoweidlem56  46594  stoweidlem57  46595  issmfle  47283  issmfgt  47294  issmfge  47308  submodaddmod  47905  fmtnoprmfac1  48138  fmtnoprmfac2  48140  clnbgredg  48426  cycl3grtrilem  48532  grlimprclnbgr  48582  grlimprclnbgredg  48583  upgrwlkupwlk  48726  copissgrp  48754  cznrng  48847  funcringcsetcALTV2lem9  48884  funcringcsetclem9ALTV  48907  linccl  49000  lincext1  49040  lincext3  49042  lincresunit2  49064  line  49318  rrxline  49320  itsclc0yqsol  49350  resipos  49560  topdlat  49589  catprs  49596  endmndlem  49600  idmon  49605  idepi  49606  thincmon  50018  thincepi  50019  grptcmon  50178  grptcepi  50179