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

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

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 1105

This theorem is referenced by:  simpr11  1276  simpr21  1279  simpr31  1282  simp1r1  1288  simp2r1  1294  simp3r1  1300  3anandis  1500  fpr2g  7211  isopolem  7345  fr3nr  7772  sexp3  8150  suppfnss  8186  frrlem4  8287  frrlem8  8291  dif1en  9147  frfi  9246  intrnfi  9377  iinfi  9378  eqsup  9417  fisupcl  9431  cnfcomlem  9669  ttrclss  9690  ackbij1lem15  10217  fpwwe2lem4  10620  dedekindle  11375  ico0  13419  elioc2  13437  elico2  13438  elicc2  13439  iccsplit  13513  fseq1p1m1  13628  elfz0ubfz0  13662  hashtpg  14524  hash7g  14525  swrdsbslen  14704  ccatswrd  14708  wwlktovf1  14996  tanadd  16224  dvds2ln  16348  qredeq  16716  ressress  17308  mreexexlem4d  17704  mreexexd  17705  0catg  17745  2oppccomf  17782  issubc3  17907  fthmon  17987  fuccocl  18025  fucidcl  18026  invfuc  18035  initoeu2lem0  18071  initoeu2lem1  18072  curf2cl  18288  yonedalem4c  18334  yonedalem3  18337  pospo  18400  latjle12  18507  latjlej1  18510  latnlej2  18516  latlem12  18523  latmlem1  18526  latledi  18534  latmlej11  18535  latjass  18540  latj12  18541  latj32  18542  latj13  18543  latj31  18544  latjrot  18545  latjjdi  18548  latjjdir  18549  latdisdlem  18553  prdssgrpd  18792  prdsmndd  18829  imasmnd2  18833  mndissubm  18866  frmdmnd  18919  grpsubrcan  19088  grpsubadd  19095  grpsubsub  19096  grpaddsubass  19097  grpsubsub4  19100  grpnnncan2  19104  imasgrp2  19122  mulgnndir  19170  mulgnn0dir  19171  mulgdir  19173  mulgnnass  19176  mulgnn0ass  19177  mulgass  19178  mulgsubdir  19181  pwsmulg  19186  issubg2  19209  eqgval  19246  qusgrp  19258  kerf1ghm  19318  galcan  19375  gacan  19376  oppgmnd  19425  pmtrprfv  19524  pmtr3ncom  19546  psgnunilem3  19567  cmn32  19871  cmn12  19873  abladdsub  19883  ablsubaddsub  19885  mulgnn0di  19896  mulgdi  19897  mulgsubdi  19900  dprdss  20102  dprdz  20103  dprdf1o  20105  dprdsn  20109  dprd2da  20115  ablfac1b  20143  pgpfac1lem5  20152  prdsrngd  20255  imasrng  20256  srgbinomlem2  20310  srgbinom  20314  ringdilem  20332  prdsringd  20403  imasring  20413  opprrng  20428  mulgass3  20436  dvrass  20491  dvrdir  20495  subrgunit  20676  issubrg2  20678  abvdiv  20913  islss3  21061  prdslmodd  21071  islmhm2  21140  lspsolv  21248  islbs2  21259  islbs3  21260  lbsextlem4  21266  sralmod  21289  prmidlc  21454  ssdifidl  21466  ipdir  21770  ipdi  21771  ipsubdir  21773  ipsubdi  21774  ipass  21776  ipassr  21777  ipassr2  21778  ocvlss  21803  psrlmod  22090  psrring  22100  psrassa  22103  ply1ass23l  22367  mamudm  22533  matring  22581  matassa  22582  ofco2  22589  mdetunilem1  22750  mdetunilem9  22758  mdetuni0  22759  mdetmul  22761  gsummatr01lem3  22795  iinopn  23040  subbascn  23392  nrmsep2  23494  isnrm3  23497  regsep2  23514  dnsconst  23516  dfconn2  23557  1stcelcls  23599  nllyidm  23627  dislly  23635  upxp  23761  fbasne0  23968  filss  23991  infil  24001  fsubbas  24005  filssufilg  24049  tmdcn2  24227  psmettri  24449  isxmet2d  24465  xmettri  24489  xmetres2  24499  bldisj  24536  blss2ps  24541  blss2  24542  xmstri2  24604  mstri2  24605  xmstri  24606  mstri  24607  xmstri3  24608  mstri3  24609  msrtri  24610  comet  24651  stdbdbl  24655  met2ndci  24660  ngprcan  24748  ngplcan  24749  ngpsubcan  24752  nmtri2  24765  nrgdsdi  24803  nrgdsdir  24804  nlmdsdi  24819  nlmdsdir  24820  blcvx  24936  icccmplem2  24962  pi1grplem  25189  pi1cof  25199  clmpm1dir  25243  cvsdiv  25272  cvsdivcl  25273  cphdivcl  25322  cphsubdir  25348  cphsubdi  25349  cphassr  25352  bcthlem5  25468  rrxcph  25532  volfiniun  25687  volcn  25746  itg1val2  25824  dvconst  26057  dvlip  26133  dvfsumlem4  26169  ftc1a  26177  ulmval  26524  ulmdvlem3  26546  ang180  26960  cvxcl  27130  scvxcvx  27131  sgmmul  27346  logexprlim  27370  dchrabl  27399  nosupbnd1  27859  noinfbnd1lem5  27872  noinfbnd1  27874  sltsss1  27939  motgrp  28793  iscgra1  29102  cgrane1  29104  cgrane2  29105  cgrahl1  29108  cgrahl2  29109  cgracgr  29110  cgratr  29115  cgrabtwn  29118  dfcgra2  29122  sacgr  29123  f1otrge  29202  colinearalglem1  29237  colinearalg  29241  axcgrtr  29246  axlowdimlem16  29288  axeuclidlem  29293  axcontlem7  29301  eengtrkg  29317  eengtrkge  29318  nbfusgrlevtxm2  29709  lfgriswlk  30017  upgrwlkdvde  30067  wwlknbp1  30174  usgrwwlks2on  30288  erclwwlktr  30354  erclwwlkntr  30403  frgr2wwlkeqm  30663  numclwwlk1lem2f  30687  numclwwlk5  30720  friendship  30731  grpodivdiv  30873  grpomuldivass  30874  ablodivdiv4  30887  ablonnncan1  30890  nvmdi  30981  dipassr  31179  archiabllem2c  33496  dvrcan5  33536  rloccring  33572  reofld  33644  eqgvscpbl  33651  qusvsval  33653  quslmod  33659  quslmhm  33660  dvdsruasso2  33680  ssmxidl  33738  ply1degltlss  33867  r1plmhm  33880  drgextlsp  33965  ccfldsrarelvec  34042  constrconj  34116  constrfin  34117  constrelextdg2  34118  pstmfval  34267  tpr2rico  34283  qqhval2lem  34352  qqhvq  34358  issiga  34483  measdivcst  34595  measdivcstALTV  34596  carsggect  34689  signsply0  34919  tgoldbachgtd  35030  bnj149  35244  bnj1118  35353  bnj1128  35359  erdszelem9  35672  resconn  35719  cvmseu  35749  cvmlift2lem12  35787  ex-sategoelel  35894  elmrsubrn  35993  mclsind  36043  r1peuqusdeg1  36116  cgrid2  36476  segconeu  36484  btwncomim  36486  btwnswapid  36490  cgrxfr  36528  btwnxfr  36529  colineardim1  36534  brofs2  36550  brifs2  36551  idinside  36557  endofsegid  36558  btwnconn1lem7  36566  btwnconn1lem11  36570  btwnconn1  36574  segcon2  36578  seglemin  36586  segletr  36587  btwnsegle  36590  colinbtwnle  36591  broutsideof2  36595  broutsideof3  36599  outsidele  36605  fvray  36614  fvline  36617  linerflx1  36622  ellines  36625  ivthALT  36827  weiunpo  36957  poimirlem32  38284  ftc1anc  38333  sdclem1  38375  sstotbnd2  38406  zerdivemp1x  38579  isdrngo2  38590  iscringd  38630  lsmsat  39763  lfladdcl  39826  lflnegcl  39830  lflvscl  39832  lshpkrlem4  39868  lshpkrlem6  39870  ldualgrplem  39900  lduallmodlem  39907  latmassOLD  39984  latm12  39985  latm32  39986  latmrot  39987  latmmdiN  39989  latmmdir  39990  omlfh1N  40013  omlfh3N  40014  cvlexchb1  40085  cvlexch3  40087  cvlexch4N  40088  cvlatexchb1  40089  cvlsupr2  40098  hlatjass  40125  hlatj12  40126  hlatj32  40127  cvratlem  40176  cvrat  40177  atcvrj0  40183  cvrat2  40184  atltcvr  40190  atexchltN  40196  cvrat3  40197  cvrat4  40198  3dimlem3  40216  3dimlem3OLDN  40217  3at  40245  2atneat  40270  llncmp  40277  2at0mat0  40280  2atmat0  40281  lplnnle2at  40296  llncvrlpln  40313  lplncmp  40317  lplnexllnN  40319  2llnjaN  40321  4atlem11  40364  lplncvrlvol  40371  lvolcmp  40372  2atm2atN  40540  elpaddatriN  40558  paddasslem9  40583  paddass  40593  padd12N  40594  paddssw2  40599  paddss  40600  pmodlem2  40602  pmodN  40605  pmapjlln1  40610  atmod1i1  40612  atmod1i2  40614  pexmidlem2N  40726  pexmidlem6N  40730  pl42N  40738  lhpm0atN  40784  lautlt  40846  lautcvr  40847  lautj  40848  lautm  40849  ltrneq2  40903  cdlemc3  40948  cdlemc4  40949  cdlemd1  40953  cdleme1b  40981  cdleme1  40982  cdleme2  40983  cdleme3e  40987  cdlemefr27cl  41158  cdlemefs27cl  41168  cdleme42mN  41242  cdlemftr2  41321  trljco  41495  tgrpgrplem  41504  tendoplass  41538  tendodi1  41539  tendodi2  41540  cdlemk36  41668  erngdvlem3  41745  erngdvlem3-rN  41753  tendospdi1  41775  dvalveclem  41780  dialss  41801  dvhvaddass  41852  dvhopvsca  41857  dvhlveclem  41863  diblss  41925  diclss  41948  dihmeetlem12N  42073  dihmeetlem15N  42076  dihmeetlem16N  42077  dihmeetlem17N  42078  dihmeetlem18N  42079  dihmeetlem19N  42080  dvh4dimN  42202  lpolvN  42241  lclkr  42288  lclkrs  42294  lcfr  42340  aks6d1c1  42864  irrapxlem6  43537  jm2.26lem3  43711  dgrsub2  43845  mpaadgr  43864  mendring  43898  mendlmod  43899  mendassa  43900  nnoeomeqom  44022  omabs2  44042  relexpmulg  44419  iunrelexpmin2  44421  relexpxpmin  44426  neicvgel1  44828  fmuldfeq  46282  stoweidlem43  46740  stoweidlem52  46749  stoweidlem53  46750  stoweidlem56  46753  stoweidlem57  46754  issmfle  47442  issmfgt  47453  issmfge  47467  submodaddmod  48067  fmtnoprmfac1  48300  fmtnoprmfac2  48302  clnbgredg  48588  cycl3grtrilem  48694  grlimprclnbgr  48744  grlimprclnbgredg  48745  upgrwlkupwlk  48888  copissgrp  48916  cznrng  49009  funcringcsetcALTV2lem9  49046  funcringcsetclem9ALTV  49069  idomcanl  49095  linccl  49177  lincext1  49217  lincext3  49219  lincresunit2  49241  line  49495  rrxline  49497  itsclc0yqsol  49527  resipos  49736  topdlat  49765  catprs  49772  endmndlem  49776  idmon  49781  idepi  49782  thincmon  50194  thincepi  50195  grptcmon  50354  grptcepi  50355