Theorem simpr1 1211

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpr11  1274  simpr21  1277  simpr31  1280  simp1r1  1286  simp2r1  1292  simp3r1  1298  3anandis  1495  fpr2g  7199  isopolem  7333  fr3nr  7759  sexp3  8137  suppfnss  8173  frrlem4  8274  frrlem8  8278  dif1en  9134  frfi  9233  intrnfi  9364  iinfi  9365  eqsup  9404  fisupcl  9418  cnfcomlem  9656  ttrclss  9677  ackbij1lem15  10204  fpwwe2lem4  10607  dedekindle  11362  ico0  13409  elioc2  13427  elico2  13428  elicc2  13429  iccsplit  13503  fseq1p1m1  13617  elfz0ubfz0  13651  hashtpg  14512  hash7g  14513  swrdsbslen  14692  ccatswrd  14696  wwlktovf1  14984  tanadd  16213  dvds2ln  16337  qredeq  16705  ressress  17297  mreexexlem4d  17693  mreexexd  17694  0catg  17734  2oppccomf  17771  issubc3  17896  fthmon  17976  fuccocl  18014  fucidcl  18015  invfuc  18024  initoeu2lem0  18060  initoeu2lem1  18061  curf2cl  18277  yonedalem4c  18323  yonedalem3  18326  pospo  18389  latjle12  18496  latjlej1  18499  latnlej2  18505  latlem12  18512  latmlem1  18515  latledi  18523  latmlej11  18524  latjass  18529  latj12  18530  latj32  18531  latj13  18532  latj31  18533  latjrot  18534  latjjdi  18537  latjjdir  18538  latdisdlem  18542  prdssgrpd  18781  prdsmndd  18818  imasmnd2  18822  mndissubm  18855  frmdmnd  18908  grpsubrcan  19078  grpsubadd  19085  grpsubsub  19086  grpaddsubass  19087  grpsubsub4  19090  grpnnncan2  19094  imasgrp2  19112  mulgnndir  19160  mulgnn0dir  19161  mulgdir  19163  mulgnnass  19166  mulgnn0ass  19167  mulgass  19168  mulgsubdir  19171  pwsmulg  19176  issubg2  19199  eqgval  19236  qusgrp  19248  kerf1ghm  19308  galcan  19365  gacan  19366  oppgmnd  19415  pmtrprfv  19514  pmtr3ncom  19536  psgnunilem3  19557  cmn32  19861  cmn12  19863  abladdsub  19873  ablsubaddsub  19875  mulgnn0di  19886  mulgdi  19887  mulgsubdi  19890  dprdss  20092  dprdz  20093  dprdf1o  20095  dprdsn  20099  dprd2da  20105  ablfac1b  20133  pgpfac1lem5  20142  prdsrngd  20245  imasrng  20246  srgbinomlem2  20300  srgbinom  20304  ringdilem  20322  prdsringd  20393  imasring  20403  opprrng  20418  mulgass3  20426  dvrass  20481  dvrdir  20485  subrgunit  20666  issubrg2  20668  abvdiv  20901  islss3  21049  prdslmodd  21059  islmhm2  21128  lspsolv  21236  islbs2  21247  islbs3  21248  lbsextlem4  21254  sralmod  21277  prmidlc  21435  ssdifidl  21445  ipdir  21749  ipdi  21750  ipsubdir  21752  ipsubdi  21753  ipass  21755  ipassr  21756  ipassr2  21757  ocvlss  21782  psrlmod  22069  psrring  22079  psrassa  22082  ply1ass23l  22346  mamudm  22513  matring  22561  matassa  22562  ofco2  22569  mdetunilem1  22730  mdetunilem9  22738  mdetuni0  22739  mdetmul  22741  gsummatr01lem3  22775  iinopn  23020  subbascn  23372  nrmsep2  23474  isnrm3  23477  regsep2  23494  dnsconst  23496  dfconn2  23537  1stcelcls  23579  nllyidm  23607  dislly  23615  upxp  23741  fbasne0  23948  filss  23971  infil  23981  fsubbas  23985  filssufilg  24029  tmdcn2  24207  psmettri  24429  isxmet2d  24445  xmettri  24469  xmetres2  24479  bldisj  24516  blss2ps  24521  blss2  24522  xmstri2  24584  mstri2  24585  xmstri  24586  mstri  24587  xmstri3  24588  mstri3  24589  msrtri  24590  comet  24631  stdbdbl  24635  met2ndci  24640  ngprcan  24728  ngplcan  24729  ngpsubcan  24732  nmtri2  24745  nrgdsdi  24783  nrgdsdir  24784  nlmdsdi  24799  nlmdsdir  24800  blcvx  24916  icccmplem2  24942  pi1grplem  25169  pi1cof  25179  clmpm1dir  25223  cvsdiv  25252  cvsdivcl  25253  cphdivcl  25302  cphsubdir  25328  cphsubdi  25329  cphassr  25332  bcthlem5  25448  rrxcph  25512  volfiniun  25667  volcn  25726  itg1val2  25804  dvconst  26037  dvlip  26113  dvfsumlem4  26149  ftc1a  26157  ulmval  26501  ulmdvlem3  26523  ang180  26937  cvxcl  27107  scvxcvx  27108  sgmmul  27323  logexprlim  27347  dchrabl  27376  nosupbnd1  27836  noinfbnd1lem5  27849  noinfbnd1  27851  sltsss1  27916  motgrp  28770  iscgra1  29062  cgrane1  29064  cgrane2  29065  cgrahl1  29068  cgrahl2  29069  cgracgr  29070  cgratr  29075  cgrabtwn  29078  dfcgra2  29082  sacgr  29083  f1otrge  29130  colinearalglem1  29165  colinearalg  29169  axcgrtr  29174  axlowdimlem16  29216  axeuclidlem  29221  axcontlem7  29229  eengtrkg  29245  eengtrkge  29246  nbfusgrlevtxm2  29637  lfgriswlk  29945  upgrwlkdvde  29995  wwlknbp1  30102  usgrwwlks2on  30216  erclwwlktr  30282  erclwwlkntr  30331  frgr2wwlkeqm  30591  numclwwlk1lem2f  30615  numclwwlk5  30648  friendship  30659  grpodivdiv  30801  grpomuldivass  30802  ablodivdiv4  30815  ablonnncan1  30818  nvmdi  30909  dipassr  31107  archiabllem2c  33428  dvrcan5  33468  rloccring  33504  reofld  33578  eqgvscpbl  33585  qusvsval  33587  quslmod  33593  quslmhm  33594  dvdsruasso2  33615  ssmxidl  33674  ply1degltlss  33803  r1plmhm  33816  drgextlsp  33901  ccfldsrarelvec  33978  constrconj  34052  constrfin  34053  constrelextdg2  34054  pstmfval  34203  tpr2rico  34219  qqhval2lem  34288  qqhvq  34294  issiga  34419  measdivcst  34531  measdivcstALTV  34532  carsggect  34625  signsply0  34855  tgoldbachgtd  34966  bnj149  35180  bnj1118  35289  bnj1128  35295  erdszelem9  35562  resconn  35609  cvmseu  35639  cvmlift2lem12  35677  ex-sategoelel  35784  elmrsubrn  35883  mclsind  35933  r1peuqusdeg1  36006  cgrid2  36366  segconeu  36374  btwncomim  36376  btwnswapid  36380  cgrxfr  36418  btwnxfr  36419  colineardim1  36424  brofs2  36440  brifs2  36441  idinside  36447  endofsegid  36448  btwnconn1lem7  36456  btwnconn1lem11  36460  btwnconn1  36464  segcon2  36468  seglemin  36476  segletr  36477  btwnsegle  36480  colinbtwnle  36481  broutsideof2  36485  broutsideof3  36489  outsidele  36495  fvray  36504  fvline  36507  linerflx1  36512  ellines  36515  ivthALT  36708  weiunpo  36838  poimirlem32  38163  ftc1anc  38212  sdclem1  38254  sstotbnd2  38285  zerdivemp1x  38458  isdrngo2  38469  iscringd  38509  lsmsat  39644  lfladdcl  39707  lflnegcl  39711  lflvscl  39713  lshpkrlem4  39749  lshpkrlem6  39751  ldualgrplem  39781  lduallmodlem  39788  latmassOLD  39865  latm12  39866  latm32  39867  latmrot  39868  latmmdiN  39870  latmmdir  39871  omlfh1N  39894  omlfh3N  39895  cvlexchb1  39966  cvlexch3  39968  cvlexch4N  39969  cvlatexchb1  39970  cvlsupr2  39979  hlatjass  40006  hlatj12  40007  hlatj32  40008  cvratlem  40057  cvrat  40058  atcvrj0  40064  cvrat2  40065  atltcvr  40071  atexchltN  40077  cvrat3  40078  cvrat4  40079  3dimlem3  40097  3dimlem3OLDN  40098  3at  40126  2atneat  40151  llncmp  40158  2at0mat0  40161  2atmat0  40162  lplnnle2at  40177  llncvrlpln  40194  lplncmp  40198  lplnexllnN  40200  2llnjaN  40202  4atlem11  40245  lplncvrlvol  40252  lvolcmp  40253  2atm2atN  40421  elpaddatriN  40439  paddasslem9  40464  paddass  40474  padd12N  40475  paddssw2  40480  paddss  40481  pmodlem2  40483  pmodN  40486  pmapjlln1  40491  atmod1i1  40493  atmod1i2  40495  pexmidlem2N  40607  pexmidlem6N  40611  pl42N  40619  lhpm0atN  40665  lautlt  40727  lautcvr  40728  lautj  40729  lautm  40730  ltrneq2  40784  cdlemc3  40829  cdlemc4  40830  cdlemd1  40834  cdleme1b  40862  cdleme1  40863  cdleme2  40864  cdleme3e  40868  cdlemefr27cl  41039  cdlemefs27cl  41049  cdleme42mN  41123  cdlemftr2  41202  trljco  41376  tgrpgrplem  41385  tendoplass  41419  tendodi1  41420  tendodi2  41421  cdlemk36  41549  erngdvlem3  41626  erngdvlem3-rN  41634  tendospdi1  41656  dvalveclem  41661  dialss  41682  dvhvaddass  41733  dvhopvsca  41738  dvhlveclem  41744  diblss  41806  diclss  41829  dihmeetlem12N  41954  dihmeetlem15N  41957  dihmeetlem16N  41958  dihmeetlem17N  41959  dihmeetlem18N  41960  dihmeetlem19N  41961  dvh4dimN  42083  lpolvN  42122  lclkr  42169  lclkrs  42175  lcfr  42221  aks6d1c1  42745  irrapxlem6  43416  jm2.26lem3  43590  dgrsub2  43724  mpaadgr  43743  mendring  43777  mendlmod  43778  mendassa  43779  nnoeomeqom  43901  omabs2  43921  relexpmulg  44298  iunrelexpmin2  44300  relexpxpmin  44305  neicvgel1  44707  fmuldfeq  46157  stoweidlem43  46615  stoweidlem52  46624  stoweidlem53  46625  stoweidlem56  46628  stoweidlem57  46629  issmfle  47317  issmfgt  47328  issmfge  47342  submodaddmod  47939  fmtnoprmfac1  48172  fmtnoprmfac2  48174  clnbgredg  48460  cycl3grtrilem  48566  grlimprclnbgr  48616  grlimprclnbgredg  48617  upgrwlkupwlk  48760  copissgrp  48788  cznrng  48881  funcringcsetcALTV2lem9  48918  funcringcsetclem9ALTV  48941  linccl  49045  lincext1  49085  lincext3  49087  lincresunit2  49109  line  49363  rrxline  49365  itsclc0yqsol  49395  resipos  49604  topdlat  49633  catprs  49640  endmndlem  49644  idmon  49649  idepi  49650  thincmon  50062  thincepi  50063  grptcmon  50222  grptcepi  50223