Theorem simpr1 1201

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpr11  1264  simpr21  1267  simpr31  1270  simp1r1  1276  simp2r1  1282  simp3r1  1288  3anandis  1479  fpr2g  7162  isopolem  7296  fr3nr  7722  sexp3  8100  suppfnss  8136  frrlem4  8236  frrlem8  8240  dif1en  9093  frfi  9192  intrnfi  9326  iinfi  9327  eqsup  9366  fisupcl  9380  cnfcomlem  9618  ttrclss  9639  ackbij1lem15  10153  fpwwe2lem4  10555  dedekindle  11308  ico0  13342  elioc2  13360  elico2  13361  elicc2  13362  iccsplit  13436  fseq1p1m1  13550  elfz0ubfz0  13584  hashtpg  14445  hash7g  14446  swrdsbslen  14625  ccatswrd  14629  wwlktovf1  14917  tanadd  16132  dvds2ln  16256  qredeq  16624  ressress  17215  mreexexlem4d  17611  mreexexd  17612  0catg  17652  2oppccomf  17689  issubc3  17814  fthmon  17894  fuccocl  17932  fucidcl  17933  invfuc  17942  initoeu2lem0  17978  initoeu2lem1  17979  curf2cl  18195  yonedalem4c  18241  yonedalem3  18244  pospo  18307  latjle12  18414  latjlej1  18417  latnlej2  18423  latlem12  18430  latmlem1  18433  latledi  18441  latmlej11  18442  latjass  18447  latj12  18448  latj32  18449  latj13  18450  latj31  18451  latjrot  18452  latjjdi  18455  latjjdir  18456  latdisdlem  18460  prdssgrpd  18699  prdsmndd  18736  imasmnd2  18740  mndissubm  18773  frmdmnd  18825  grpsubrcan  18995  grpsubadd  19002  grpsubsub  19003  grpaddsubass  19004  grpsubsub4  19007  grpnnncan2  19011  imasgrp2  19029  mulgnndir  19077  mulgnn0dir  19078  mulgdir  19080  mulgnnass  19083  mulgnn0ass  19084  mulgass  19085  mulgsubdir  19088  pwsmulg  19093  issubg2  19115  eqgval  19150  qusgrp  19159  kerf1ghm  19220  galcan  19277  gacan  19278  oppgmnd  19327  pmtrprfv  19426  pmtr3ncom  19448  psgnunilem3  19469  cmn32  19773  cmn12  19775  abladdsub  19785  ablsubaddsub  19787  mulgnn0di  19798  mulgdi  19799  mulgsubdi  19802  dprdss  20004  dprdz  20005  dprdf1o  20007  dprdsn  20011  dprd2da  20017  ablfac1b  20045  pgpfac1lem5  20054  prdsrngd  20155  imasrng  20156  srgbinomlem2  20206  srgbinom  20210  ringdilem  20228  prdsringd  20298  imasring  20308  opprrng  20323  mulgass3  20331  dvrass  20386  dvrdir  20390  subrgunit  20569  issubrg2  20571  abvdiv  20808  islss3  20956  prdslmodd  20966  islmhm2  21035  lspsolv  21143  islbs2  21154  islbs3  21155  lbsextlem4  21161  sralmod  21184  ipdir  21621  ipdi  21622  ipsubdir  21624  ipsubdi  21625  ipass  21627  ipassr  21628  ipassr2  21629  ocvlss  21654  psrlmod  21941  psrring  21951  psrassa  21954  ply1ass23l  22218  mamudm  22385  matring  22433  matassa  22434  ofco2  22441  mdetunilem1  22602  mdetunilem9  22610  mdetuni0  22611  mdetmul  22613  gsummatr01lem3  22647  iinopn  22892  subbascn  23244  nrmsep2  23346  isnrm3  23349  regsep2  23366  dnsconst  23368  dfconn2  23409  1stcelcls  23451  nllyidm  23479  dislly  23487  upxp  23613  fbasne0  23820  filss  23843  infil  23853  fsubbas  23857  filssufilg  23901  tmdcn2  24079  psmettri  24301  isxmet2d  24317  xmettri  24341  xmetres2  24351  bldisj  24388  blss2ps  24393  blss2  24394  xmstri2  24456  mstri2  24457  xmstri  24458  mstri  24459  xmstri3  24460  mstri3  24461  msrtri  24462  comet  24503  stdbdbl  24507  met2ndci  24512  ngprcan  24600  ngplcan  24601  ngpsubcan  24604  nmtri2  24617  nrgdsdi  24655  nrgdsdir  24656  nlmdsdi  24671  nlmdsdir  24672  blcvx  24788  icccmplem2  24814  pi1grplem  25041  pi1cof  25051  clmpm1dir  25095  cvsdiv  25124  cvsdivcl  25125  cphdivcl  25174  cphsubdir  25200  cphsubdi  25201  cphassr  25204  bcthlem5  25320  rrxcph  25384  volfiniun  25539  volcn  25598  itg1val2  25676  dvconst  25909  dvlip  25985  dvfsumlem4  26021  ftc1a  26029  ulmval  26370  ulmdvlem3  26392  ang180  26803  cvxcl  26973  scvxcvx  26974  sgmmul  27189  logexprlim  27213  dchrabl  27242  nosupbnd1  27703  noinfbnd1lem5  27716  noinfbnd1  27718  sltsss1  27782  motgrp  28636  iscgra1  28903  cgrane1  28905  cgrane2  28906  cgrahl1  28909  cgrahl2  28910  cgracgr  28911  cgratr  28916  cgrabtwn  28919  dfcgra2  28923  sacgr  28924  f1otrge  28965  colinearalglem1  29000  colinearalg  29004  axcgrtr  29009  axlowdimlem16  29051  axeuclidlem  29056  axcontlem7  29064  eengtrkg  29080  eengtrkge  29081  nbfusgrlevtxm2  29472  lfgriswlk  29780  upgrwlkdvde  29830  wwlknbp1  29937  usgrwwlks2on  30051  erclwwlktr  30117  erclwwlkntr  30166  frgr2wwlkeqm  30426  numclwwlk1lem2f  30450  numclwwlk5  30483  friendship  30494  grpodivdiv  30636  grpomuldivass  30637  ablodivdiv4  30650  ablonnncan1  30653  nvmdi  30744  dipassr  30942  archiabllem2c  33283  dvrcan5  33324  rloccring  33358  reofld  33433  eqgvscpbl  33440  qusvsval  33442  quslmod  33448  quslmhm  33449  dvdsruasso2  33476  prmidlc  33538  ssdifidl  33547  ssmxidl  33564  ply1degltlss  33686  r1plmhm  33700  drgextlsp  33785  ccfldsrarelvec  33862  constrconj  33936  constrfin  33937  constrelextdg2  33938  pstmfval  34087  tpr2rico  34103  qqhval2lem  34172  qqhvq  34178  issiga  34303  measdivcst  34415  measdivcstALTV  34416  carsggect  34509  signsply0  34742  tgoldbachgtd  34853  bnj149  35064  bnj1118  35173  bnj1128  35179  erdszelem9  35434  resconn  35481  cvmseu  35511  cvmlift2lem12  35549  ex-sategoelel  35656  elmrsubrn  35755  mclsind  35805  r1peuqusdeg1  35878  cgrid2  36238  segconeu  36246  btwncomim  36248  btwnswapid  36252  cgrxfr  36290  btwnxfr  36291  colineardim1  36296  brofs2  36312  brifs2  36313  idinside  36319  endofsegid  36320  btwnconn1lem7  36328  btwnconn1lem11  36332  btwnconn1  36336  segcon2  36340  seglemin  36348  segletr  36349  btwnsegle  36352  colinbtwnle  36353  broutsideof2  36357  broutsideof3  36361  outsidele  36367  fvray  36376  fvline  36379  linerflx1  36384  ellines  36387  ivthALT  36570  weiunpo  36700  poimirlem32  38026  ftc1anc  38075  sdclem1  38117  sstotbnd2  38148  zerdivemp1x  38321  isdrngo2  38332  iscringd  38372  lsmsat  39507  lfladdcl  39570  lflnegcl  39574  lflvscl  39576  lshpkrlem4  39612  lshpkrlem6  39614  ldualgrplem  39644  lduallmodlem  39651  latmassOLD  39728  latm12  39729  latm32  39730  latmrot  39731  latmmdiN  39733  latmmdir  39734  omlfh1N  39757  omlfh3N  39758  cvlexchb1  39829  cvlexch3  39831  cvlexch4N  39832  cvlatexchb1  39833  cvlsupr2  39842  hlatjass  39869  hlatj12  39870  hlatj32  39871  cvratlem  39920  cvrat  39921  atcvrj0  39927  cvrat2  39928  atltcvr  39934  atexchltN  39940  cvrat3  39941  cvrat4  39942  3dimlem3  39960  3dimlem3OLDN  39961  3at  39989  2atneat  40014  llncmp  40021  2at0mat0  40024  2atmat0  40025  lplnnle2at  40040  llncvrlpln  40057  lplncmp  40061  lplnexllnN  40063  2llnjaN  40065  4atlem11  40108  lplncvrlvol  40115  lvolcmp  40116  2atm2atN  40284  elpaddatriN  40302  paddasslem9  40327  paddass  40337  padd12N  40338  paddssw2  40343  paddss  40344  pmodlem2  40346  pmodN  40349  pmapjlln1  40354  atmod1i1  40356  atmod1i2  40358  pexmidlem2N  40470  pexmidlem6N  40474  pl42N  40482  lhpm0atN  40528  lautlt  40590  lautcvr  40591  lautj  40592  lautm  40593  ltrneq2  40647  cdlemc3  40692  cdlemc4  40693  cdlemd1  40697  cdleme1b  40725  cdleme1  40726  cdleme2  40727  cdleme3e  40731  cdlemefr27cl  40902  cdlemefs27cl  40912  cdleme42mN  40986  cdlemftr2  41065  trljco  41239  tgrpgrplem  41248  tendoplass  41282  tendodi1  41283  tendodi2  41284  cdlemk36  41412  erngdvlem3  41489  erngdvlem3-rN  41497  tendospdi1  41519  dvalveclem  41524  dialss  41545  dvhvaddass  41596  dvhopvsca  41601  dvhlveclem  41607  diblss  41669  diclss  41692  dihmeetlem12N  41817  dihmeetlem15N  41820  dihmeetlem16N  41821  dihmeetlem17N  41822  dihmeetlem18N  41823  dihmeetlem19N  41824  dvh4dimN  41946  lpolvN  41985  lclkr  42032  lclkrs  42038  lcfr  42084  aks6d1c1  42608  irrapxlem6  43279  jm2.26lem3  43453  dgrsub2  43587  mpaadgr  43606  mendring  43640  mendlmod  43641  mendassa  43642  nnoeomeqom  43764  omabs2  43784  relexpmulg  44161  iunrelexpmin2  44163  relexpxpmin  44168  neicvgel1  44570  fmuldfeq  46035  stoweidlem43  46493  stoweidlem52  46502  stoweidlem53  46503  stoweidlem56  46506  stoweidlem57  46507  issmfle  47195  issmfgt  47206  issmfge  47220  submodaddmod  47817  fmtnoprmfac1  48050  fmtnoprmfac2  48052  clnbgredg  48338  cycl3grtrilem  48444  grlimprclnbgr  48494  grlimprclnbgredg  48495  upgrwlkupwlk  48638  copissgrp  48666  cznrng  48759  funcringcsetcALTV2lem9  48796  funcringcsetclem9ALTV  48819  linccl  48912  lincext1  48952  lincext3  48954  lincresunit2  48976  line  49230  rrxline  49232  itsclc0yqsol  49262  resipos  49472  topdlat  49501  catprs  49508  endmndlem  49512  idmon  49517  idepi  49518  thincmon  49930  thincepi  49931  grptcmon  50090  grptcepi  50091