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  7151  isopolem  7286  fr3nr  7712  sexp3  8093  suppfnss  8129  frrlem4  8229  frrlem8  8233  dif1en  9084  frfi  9190  intrnfi  9325  iinfi  9326  eqsup  9365  fisupcl  9379  cnfcomlem  9614  ttrclss  9635  ackbij1lem15  10146  fpwwe2lem4  10547  dedekindle  11298  ico0  13312  elioc2  13330  elico2  13331  elicc2  13332  iccsplit  13406  fseq1p1m1  13519  elfz0ubfz0  13553  hashtpg  14410  hash7g  14411  swrdsbslen  14589  ccatswrd  14593  wwlktovf1  14882  tanadd  16094  dvds2ln  16218  qredeq  16586  ressress  17176  mreexexlem4d  17571  mreexexd  17572  0catg  17612  2oppccomf  17649  issubc3  17774  fthmon  17854  fuccocl  17892  fucidcl  17893  invfuc  17902  initoeu2lem0  17938  initoeu2lem1  17939  curf2cl  18155  yonedalem4c  18201  yonedalem3  18204  pospo  18267  latjle12  18374  latjlej1  18377  latnlej2  18383  latlem12  18390  latmlem1  18393  latledi  18401  latmlej11  18402  latjass  18407  latj12  18408  latj32  18409  latj13  18410  latj31  18411  latjrot  18412  latjjdi  18415  latjjdir  18416  latdisdlem  18420  prdssgrpd  18625  prdsmndd  18662  imasmnd2  18666  mndissubm  18699  frmdmnd  18751  grpsubrcan  18918  grpsubadd  18925  grpsubsub  18926  grpaddsubass  18927  grpsubsub4  18930  grpnnncan2  18934  imasgrp2  18952  mulgnndir  19000  mulgnn0dir  19001  mulgdir  19003  mulgnnass  19006  mulgnn0ass  19007  mulgass  19008  mulgsubdir  19011  pwsmulg  19016  issubg2  19038  eqgval  19074  qusgrp  19083  kerf1ghm  19144  galcan  19201  gacan  19202  oppgmnd  19251  pmtrprfv  19350  pmtr3ncom  19372  psgnunilem3  19393  cmn32  19697  cmn12  19699  abladdsub  19709  ablsubaddsub  19711  mulgnn0di  19722  mulgdi  19723  mulgsubdi  19726  dprdss  19928  dprdz  19929  dprdf1o  19931  dprdsn  19935  dprd2da  19941  ablfac1b  19969  pgpfac1lem5  19978  prdsrngd  20079  imasrng  20080  srgbinomlem2  20130  srgbinom  20134  ringdilem  20152  prdsringd  20224  imasring  20233  opprrng  20248  mulgass3  20256  dvrass  20311  dvrdir  20315  subrgunit  20493  issubrg2  20495  abvdiv  20732  islss3  20880  prdslmodd  20890  islmhm2  20960  lspsolv  21068  islbs2  21079  islbs3  21080  lbsextlem4  21086  sralmod  21109  ipdir  21564  ipdi  21565  ipsubdir  21567  ipsubdi  21568  ipass  21570  ipassr  21571  ipassr2  21572  ocvlss  21597  sraassaOLD  21795  psrgrpOLD  21882  psrlmod  21885  psrring  21895  psrassa  21898  ply1ass23l  22127  mamudm  22298  matring  22346  matassa  22347  ofco2  22354  mdetunilem1  22515  mdetunilem9  22523  mdetuni0  22524  mdetmul  22526  gsummatr01lem3  22560  iinopn  22805  subbascn  23157  nrmsep2  23259  isnrm3  23262  regsep2  23279  dnsconst  23281  dfconn2  23322  1stcelcls  23364  nllyidm  23392  dislly  23400  upxp  23526  fbasne0  23733  filss  23756  infil  23766  fsubbas  23770  filssufilg  23814  tmdcn2  23992  psmettri  24215  isxmet2d  24231  xmettri  24255  xmetres2  24265  bldisj  24302  blss2ps  24307  blss2  24308  xmstri2  24370  mstri2  24371  xmstri  24372  mstri  24373  xmstri3  24374  mstri3  24375  msrtri  24376  comet  24417  stdbdbl  24421  met2ndci  24426  ngprcan  24514  ngplcan  24515  ngpsubcan  24518  nmtri2  24531  nrgdsdi  24569  nrgdsdir  24570  nlmdsdi  24585  nlmdsdir  24586  blcvx  24702  icccmplem2  24728  pi1grplem  24965  pi1cof  24975  clmpm1dir  25019  cvsdiv  25048  cvsdivcl  25049  cphdivcl  25098  cphsubdir  25124  cphsubdi  25125  cphassr  25128  bcthlem5  25244  rrxcph  25308  volfiniun  25464  volcn  25523  itg1val2  25601  dvconst  25834  dvlip  25914  dvfsumlem4  25952  ftc1a  25960  ulmval  26305  ulmdvlem3  26327  ang180  26740  cvxcl  26911  scvxcvx  26912  sgmmul  27128  logexprlim  27152  dchrabl  27181  nosupbnd1  27642  noinfbnd1lem5  27655  noinfbnd1  27657  ssltss1  27717  motgrp  28506  iscgra1  28773  cgrane1  28775  cgrane2  28776  cgrahl1  28779  cgrahl2  28780  cgracgr  28781  cgratr  28786  cgrabtwn  28789  dfcgra2  28793  sacgr  28794  f1otrge  28835  colinearalglem1  28869  colinearalg  28873  axcgrtr  28878  axlowdimlem16  28920  axeuclidlem  28925  axcontlem7  28933  eengtrkg  28949  eengtrkge  28950  nbfusgrlevtxm2  29341  lfgriswlk  29650  upgrwlkdvde  29700  wwlknbp1  29807  erclwwlktr  29984  erclwwlkntr  30033  frgr2wwlkeqm  30293  numclwwlk1lem2f  30317  numclwwlk5  30350  friendship  30361  grpodivdiv  30502  grpomuldivass  30503  ablodivdiv4  30516  ablonnncan1  30519  nvmdi  30610  dipassr  30808  archiabllem2c  33147  dvrcan5  33186  rloccring  33220  reofld  33291  eqgvscpbl  33297  qusvsval  33299  quslmod  33305  quslmhm  33306  dvdsruasso2  33333  prmidlc  33395  ssdifidl  33404  ssmxidl  33421  ply1degltlss  33538  r1plmhm  33551  drgextlsp  33565  ccfldsrarelvec  33642  constrconj  33711  constrfin  33712  constrelextdg2  33713  pstmfval  33862  tpr2rico  33878  qqhval2lem  33947  qqhvq  33953  issiga  34078  measdivcst  34190  measdivcstALTV  34191  carsggect  34285  signsply0  34518  tgoldbachgtd  34629  bnj149  34841  bnj1118  34950  bnj1128  34956  erdszelem9  35171  resconn  35218  cvmseu  35248  cvmlift2lem12  35286  ex-sategoelel  35393  elmrsubrn  35492  mclsind  35542  r1peuqusdeg1  35615  cgrid2  35976  segconeu  35984  btwncomim  35986  btwnswapid  35990  cgrxfr  36028  btwnxfr  36029  colineardim1  36034  brofs2  36050  brifs2  36051  idinside  36057  endofsegid  36058  btwnconn1lem7  36066  btwnconn1lem11  36070  btwnconn1  36074  segcon2  36078  seglemin  36086  segletr  36087  btwnsegle  36090  colinbtwnle  36091  broutsideof2  36095  broutsideof3  36099  outsidele  36105  fvray  36114  fvline  36117  linerflx1  36122  ellines  36125  ivthALT  36308  weiunpo  36438  poimirlem32  37631  ftc1anc  37680  sdclem1  37722  sstotbnd2  37753  zerdivemp1x  37926  isdrngo2  37937  iscringd  37977  lsmsat  38986  lfladdcl  39049  lflnegcl  39053  lflvscl  39055  lshpkrlem4  39091  lshpkrlem6  39093  ldualgrplem  39123  lduallmodlem  39130  latmassOLD  39207  latm12  39208  latm32  39209  latmrot  39210  latmmdiN  39212  latmmdir  39213  omlfh1N  39236  omlfh3N  39237  cvlexchb1  39308  cvlexch3  39310  cvlexch4N  39311  cvlatexchb1  39312  cvlsupr2  39321  hlatjass  39348  hlatj12  39349  hlatj32  39350  cvratlem  39400  cvrat  39401  atcvrj0  39407  cvrat2  39408  atltcvr  39414  atexchltN  39420  cvrat3  39421  cvrat4  39422  3dimlem3  39440  3dimlem3OLDN  39441  3at  39469  2atneat  39494  llncmp  39501  2at0mat0  39504  2atmat0  39505  lplnnle2at  39520  llncvrlpln  39537  lplncmp  39541  lplnexllnN  39543  2llnjaN  39545  4atlem11  39588  lplncvrlvol  39595  lvolcmp  39596  2atm2atN  39764  elpaddatriN  39782  paddasslem9  39807  paddass  39817  padd12N  39818  paddssw2  39823  paddss  39824  pmodlem2  39826  pmodN  39829  pmapjlln1  39834  atmod1i1  39836  atmod1i2  39838  pexmidlem2N  39950  pexmidlem6N  39954  pl42N  39962  lhpm0atN  40008  lautlt  40070  lautcvr  40071  lautj  40072  lautm  40073  ltrneq2  40127  cdlemc3  40172  cdlemc4  40173  cdlemd1  40177  cdleme1b  40205  cdleme1  40206  cdleme2  40207  cdleme3e  40211  cdlemefr27cl  40382  cdlemefs27cl  40392  cdleme42mN  40466  cdlemftr2  40545  trljco  40719  tgrpgrplem  40728  tendoplass  40762  tendodi1  40763  tendodi2  40764  cdlemk36  40892  erngdvlem3  40969  erngdvlem3-rN  40977  tendospdi1  40999  dvalveclem  41004  dialss  41025  dvhvaddass  41076  dvhopvsca  41081  dvhlveclem  41087  diblss  41149  diclss  41172  dihmeetlem12N  41297  dihmeetlem15N  41300  dihmeetlem16N  41301  dihmeetlem17N  41302  dihmeetlem18N  41303  dihmeetlem19N  41304  dvh4dimN  41426  lpolvN  41465  lclkr  41512  lclkrs  41518  lcfr  41564  aks6d1c1  42089  irrapxlem6  42800  jm2.26lem3  42974  dgrsub2  43108  mpaadgr  43127  mendring  43161  mendlmod  43162  mendassa  43163  nnoeomeqom  43285  omabs2  43305  relexpmulg  43683  iunrelexpmin2  43685  relexpxpmin  43690  neicvgel1  44092  fmuldfeq  45565  stoweidlem43  46025  stoweidlem52  46034  stoweidlem53  46035  stoweidlem56  46038  stoweidlem57  46039  issmfle  46727  issmfgt  46738  issmfge  46752  submodaddmod  47326  fmtnoprmfac1  47550  fmtnoprmfac2  47552  clnbgredg  47825  cycl3grtrilem  47931  grlimprclnbgr  47981  grlimprclnbgredg  47982  upgrwlkupwlk  48125  copissgrp  48153  cznrng  48246  funcringcsetcALTV2lem9  48283  funcringcsetclem9ALTV  48306  linccl  48400  lincext1  48440  lincext3  48442  lincresunit2  48464  line  48718  rrxline  48720  itsclc0yqsol  48750  resipos  48960  topdlat  48989  catprs  48997  endmndlem  49001  idmon  49006  idepi  49007  thincmon  49419  thincepi  49420  grptcmon  49579  grptcepi  49580