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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr11  1276  simpr21  1279  simpr31  1282  simp1r1  1288  simp2r1  1294  simp3r1  1300  3anandis  1500  fpr2g  7209  isopolem  7345  fr3nr  7775  sexp3  8154  suppfnss  8190  frrlem4  8291  frrlem8  8295  dif1en  9161  frfi  9260  intrnfi  9392  iinfi  9393  eqsup  9432  fisupcl  9446  cnfcomlem  9684  ttrclss  9705  ackbij1lem15  10292  fpwwe2lem4  10700  dedekindle  11455  ico0  13503  elioc2  13521  elico2  13522  elicc2  13523  iccsplit  13597  fseq1p1m1  13712  elfz0ubfz0  13746  hashtpg  14610  hash7g  14611  swrdsbslen  14794  ccatswrd  14798  wwlktovf1  15090  tanadd  16315  dvds2ln  16439  qredeq  16812  ressress  17405  mreexexlem4d  17801  mreexexd  17802  0catg  17842  2oppccomf  17879  issubc3  18004  fthmon  18084  fuccocl  18122  fucidcl  18123  invfuc  18132  initoeu2lem0  18168  initoeu2lem1  18169  curf2cl  18385  yonedalem4c  18431  yonedalem3  18434  pospo  18497  latjle12  18604  latjlej1  18607  latnlej2  18613  latlem12  18620  latmlem1  18623  latledi  18631  latmlej11  18632  latjass  18637  latj12  18638  latj32  18639  latj13  18640  latj31  18641  latjrot  18642  latjjdi  18645  latjjdir  18646  latdisdlem  18650  prdssgrpd  18902  prdsmndd  18944  imasmnd2  18948  mndissubm  18982  frmdmnd  19035  grpsubrcan  19211  grpsubadd  19218  grpsubsub  19219  grpaddsubass  19220  grpsubsub4  19223  grpnnncan2  19227  imasgrp2  19245  mulgnndir  19293  mulgnn0dir  19294  mulgdir  19296  mulgnnass  19299  mulgnn0ass  19300  mulgass  19301  mulgsubdir  19304  pwsmulg  19309  issubg2  19332  eqgval  19369  qusgrp  19381  kerf1ghm  19441  galcan  19498  gacan  19499  oppgmnd  19548  pmtrprfv  19647  pmtr3ncom  19669  psgnunilem3  19690  cmn32  19994  cmn12  19996  abladdsub  20006  ablsubaddsub  20008  mulgnn0di  20019  mulgdi  20020  mulgsubdi  20023  dprdss  20225  dprdz  20226  dprdf1o  20228  dprdsn  20232  dprd2da  20238  ablfac1b  20266  pgpfac1lem5  20275  prdsrngd  20378  imasrng  20379  srgbinomlem2  20433  srgbinom  20437  ringdilem  20456  prdsringd  20530  imasring  20540  opprrng  20555  mulgass3  20563  dvrass  20618  dvrdir  20622  subrgunit  20822  issubrg2  20824  abvdiv  21066  islss3  21214  prdslmodd  21224  islmhm2  21293  lspsolv  21401  islbs2  21412  islbs3  21413  lbsextlem4  21419  sralmod  21442  prmidlc  21609  ssdifidl  21621  ipdir  21925  ipdi  21926  ipsubdir  21928  ipsubdi  21929  ipass  21931  ipassr  21932  ipassr2  21933  ocvlss  21958  psrlmod  22247  psrring  22257  psrassa  22260  ply1ass23l  22524  mamudm  22690  matring  22738  matassa  22739  ofco2  22746  mdetunilem1  22907  mdetunilem9  22915  mdetuni0  22916  mdetmul  22918  gsummatr01lem3  22952  iinopn  23200  subbascn  23552  nrmsep2  23654  isnrm3  23657  regsep2  23674  dnsconst  23676  dfconn2  23717  1stcelcls  23760  nllyidm  23788  dislly  23796  upxp  23922  fbasne0  24129  filss  24152  infil  24162  fsubbas  24166  filssufilg  24210  tmdcn2  24388  psmettri  24610  isxmet2d  24626  xmettri  24650  xmetres2  24660  bldisj  24697  blss2ps  24702  blss2  24703  xmstri2  24765  mstri2  24766  xmstri  24767  mstri  24768  xmstri3  24769  mstri3  24770  msrtri  24771  comet  24812  stdbdbl  24816  met2ndci  24821  ngprcan  24909  ngplcan  24910  ngpsubcan  24913  nmtri2  24926  nrgdsdi  24964  nrgdsdir  24965  nlmdsdi  24980  nlmdsdir  24981  blcvx  25097  icccmplem2  25123  pi1grplem  25350  pi1cof  25360  clmpm1dir  25404  cvsdiv  25433  cvsdivcl  25434  cphdivcl  25483  cphsubdir  25509  cphsubdi  25510  cphassr  25513  bcthlem5  25629  rrxcph  25693  volfiniun  25848  volcn  25907  itg1val2  25985  dvconst  26217  dvlip  26293  dvfsumlem4  26329  ftc1a  26337  ulmval  26689  ulmdvlem3  26711  ang180  27124  cvxcl  27294  scvxcvx  27295  sgmmul  27510  logexprlim  27534  dchrabl  27563  nosupbnd1  28053  noinfbnd1lem5  28066  noinfbnd1  28068  sltsss1  28133  motgrp  28988  iscgra1  29299  cgrane1  29301  cgrane2  29302  cgrahl1  29305  cgrahl2  29306  cgracgr  29307  cgratr  29312  cgrabtwn  29316  dfcgra2  29320  sacgr  29321  angmgmaddcl  29373  f1otrge  29431  colinearalglem1  29466  colinearalg  29470  axcgrtr  29475  axlowdimlem16  29517  axeuclidlem  29522  axcontlem7  29530  eengtrkg  29546  eengtrkge  29547  nbfusgrlevtxm2  29941  lfgriswlk  30253  upgrwlkdvde  30305  wwlknbp1  30415  usgrwwlks2on  30529  erclwwlktr  30595  erclwwlkntr  30644  frgr2wwlkeqm  30914  numclwwlk1lem2f  30938  numclwwlk5  30971  friendship  30982  grpodivdiv  31124  grpomuldivass  31125  ablodivdiv4  31138  ablonnncan1  31141  nvmdi  31232  dipassr  31430  archiabllem2c  33738  dvrcan5  33778  rloccring  33814  reofld  33886  eqgvscpbl  33893  qusvsval  33895  quslmod  33901  quslmhm  33902  dvdsruasso2  33923  ssmxidl  33981  ply1degltlss  34110  r1plmhm  34123  drgextlsp  34208  ccfldsrarelvec  34285  constrconj  34359  constrfin  34360  constrelextdg2  34361  pstmfval  34510  tpr2rico  34526  qqhval2lem  34595  qqhvq  34601  issiga  34726  measdivcst  34839  measdivcstALTV  34840  carsggect  34933  signsply0  35163  tgoldbachgtd  35274  bnj149  35488  bnj1118  35597  bnj1128  35603  erdszelem9  35933  resconn  35980  cvmseu  36010  cvmlift2lem12  36048  ex-sategoelel  36155  elmrsubrn  36254  mclsind  36304  r1peuqusdeg1  36377  cgrid2  36738  segconeu  36746  btwncomim  36748  btwnswapid  36752  cgrxfr  36790  btwnxfr  36791  colineardim1  36796  brofs2  36812  brifs2  36813  idinside  36819  endofsegid  36820  btwnconn1lem7  36828  btwnconn1lem11  36832  btwnconn1  36836  segcon2  36840  seglemin  36848  segletr  36849  btwnsegle  36852  colinbtwnle  36853  broutsideof2  36857  broutsideof3  36861  outsidele  36867  fvray  36876  fvline  36879  linerflx1  36884  ellines  36887  ivthALT  37093  weiunpo  37223  poimirlem32  38538  ftc1anc  38587  sdclem1  38645  sstotbnd2  38676  zerdivemp1x  38849  isdrngo2  38860  iscringd  38900  lsmsat  40033  lfladdcl  40096  lflnegcl  40100  lflvscl  40102  lshpkrlem4  40138  lshpkrlem6  40140  ldualgrplem  40170  lduallmodlem  40177  latmassOLD  40254  latm12  40255  latm32  40256  latmrot  40257  latmmdiN  40259  latmmdir  40260  omlfh1N  40283  omlfh3N  40284  cvlexchb1  40355  cvlexch3  40357  cvlexch4N  40358  cvlatexchb1  40359  cvlsupr2  40368  hlatjass  40395  hlatj12  40396  hlatj32  40397  cvratlem  40446  cvrat  40447  atcvrj0  40453  cvrat2  40454  atltcvr  40460  atexchltN  40466  cvrat3  40467  cvrat4  40468  3dimlem3  40486  3dimlem3OLDN  40487  3at  40515  2atneat  40540  llncmp  40547  2at0mat0  40550  2atmat0  40551  lplnnle2at  40566  llncvrlpln  40583  lplncmp  40587  lplnexllnN  40589  2llnjaN  40591  4atlem11  40634  lplncvrlvol  40641  lvolcmp  40642  2atm2atN  40810  elpaddatriN  40828  paddasslem9  40853  paddass  40863  padd12N  40864  paddssw2  40869  paddss  40870  pmodlem2  40872  pmodN  40875  pmapjlln1  40880  atmod1i1  40882  atmod1i2  40884  pexmidlem2N  40996  pexmidlem6N  41000  pl42N  41008  lhpm0atN  41054  lautlt  41116  lautcvr  41117  lautj  41118  lautm  41119  ltrneq2  41173  cdlemc3  41218  cdlemc4  41219  cdlemd1  41223  cdleme1b  41251  cdleme1  41252  cdleme2  41253  cdleme3e  41257  cdlemefr27cl  41428  cdlemefs27cl  41438  cdleme42mN  41512  cdlemftr2  41591  trljco  41765  tgrpgrplem  41774  tendoplass  41808  tendodi1  41809  tendodi2  41810  cdlemk36  41938  erngdvlem3  42015  erngdvlem3-rN  42023  tendospdi1  42045  dvalveclem  42050  dialss  42071  dvhvaddass  42122  dvhopvsca  42127  dvhlveclem  42133  diblss  42195  diclss  42218  dihmeetlem12N  42343  dihmeetlem15N  42346  dihmeetlem16N  42347  dihmeetlem17N  42348  dihmeetlem18N  42349  dihmeetlem19N  42350  dvh4dimN  42472  lpolvN  42511  lclkr  42558  lclkrs  42564  lcfr  42610  aks6d1c1  43134  irrapxlem6  43787  jm2.26lem3  43961  dgrsub2  44095  mpaadgr  44114  mendring  44148  mendlmod  44149  mendassa  44150  nnoeomeqom  44272  omabs2  44292  relexpmulg  44669  iunrelexpmin2  44671  relexpxpmin  44676  neicvgel1  45078  fmuldfeq  46539  stoweidlem43  46997  stoweidlem52  47006  stoweidlem53  47007  stoweidlem56  47010  stoweidlem57  47011  issmfle  47699  issmfgt  47710  issmfge  47724  submodaddmod  48361  fmtnoprmfac1  48594  fmtnoprmfac2  48596  clnbgredg  48882  cycl3grtrilem  48988  grlimprclnbgr  49038  grlimprclnbgredg  49039  upgrwlkupwlk  49182  copissgrp  49209  cznrng  49302  funcringcsetcALTV2lem9  49339  funcringcsetclem9ALTV  49362  idomcanl  49388  linccl  49470  lincext1  49510  lincext3  49512  lincresunit2  49534  line  49788  rrxline  49790  itsclc0yqsol  49820  resipos  50027  topdlat  50056  catprs  50063  endmndlem  50067  idmon  50072  idepi  50073  thincmon  50485  thincepi  50486  grptcmon  50645  grptcepi  50646  nellindf  50914