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  1501  fpr2g  7243  isopolem  7379  fr3nr  7813  sexp3  8200  suppfnss  8237  frrlem4  8338  frrlem8  8342  dif1en  9208  frfi  9307  intrnfi  9438  iinfi  9439  eqsup  9478  fisupcl  9492  cnfcomlem  9730  ttrclss  9751  ackbij1lem15  10341  fpwwe2lem4  10749  dedekindle  11504  ico0  13552  elioc2  13570  elico2  13571  elicc2  13572  iccsplit  13646  fseq1p1m1  13762  elfz0ubfz0  13796  hashtpg  14660  hash7g  14661  swrdsbslen  14845  ccatswrd  14849  wwlktovf1  15142  tanadd  16367  dvds2ln  16491  qredeq  16864  ressress  17457  mreexexlem4d  17853  mreexexd  17854  0catg  17894  2oppccomf  17931  issubc3  18056  fthmon  18136  fuccocl  18174  fucidcl  18175  invfuc  18184  initoeu2lem0  18220  initoeu2lem1  18221  curf2cl  18437  yonedalem4c  18483  yonedalem3  18486  pospo  18549  latjle12  18656  latjlej1  18659  latnlej2  18665  latlem12  18672  latmlem1  18675  latledi  18683  latmlej11  18684  latjass  18689  latj12  18690  latj32  18691  latj13  18692  latj31  18693  latjrot  18694  latjjdi  18697  latjjdir  18698  latdisdlem  18702  prdssgrpd  18954  prdsmndd  18996  imasmnd2  19000  mndissubm  19034  frmdmnd  19087  grpsubrcan  19263  grpsubadd  19270  grpsubsub  19271  grpaddsubass  19272  grpsubsub4  19275  grpnnncan2  19279  imasgrp2  19297  mulgnndir  19345  mulgnn0dir  19346  mulgdir  19348  mulgnnass  19351  mulgnn0ass  19352  mulgass  19353  mulgsubdir  19356  pwsmulg  19361  issubg2  19384  eqgval  19421  qusgrp  19433  kerf1ghm  19493  galcan  19551  gacan  19552  oppgmnd  19601  pmtrprfv  19700  pmtr3ncom  19722  psgnunilem3  19743  cmn32  20047  cmn12  20049  abladdsub  20059  ablsubaddsub  20061  mulgnn0di  20072  mulgdi  20073  mulgsubdi  20076  dprdss  20278  dprdz  20279  dprdf1o  20281  dprdsn  20285  dprd2da  20291  ablfac1b  20319  pgpfac1lem5  20328  prdsrngd  20431  imasrng  20432  srgbinomlem2  20486  srgbinom  20490  ringdilem  20509  prdsringd  20583  imasring  20593  opprrng  20608  mulgass3  20616  dvrass  20671  dvrdir  20675  subrgunit  20875  issubrg2  20877  abvdiv  21119  islss3  21267  prdslmodd  21277  islmhm2  21346  lspsolv  21454  islbs2  21465  islbs3  21466  lbsextlem4  21472  sralmod  21495  prmidlc  21662  ssdifidl  21674  ipdir  21978  ipdi  21979  ipsubdir  21981  ipsubdi  21982  ipass  21984  ipassr  21985  ipassr2  21986  ocvlss  22011  psrlmod  22300  psrring  22310  psrassa  22313  ply1ass23l  22577  mamudm  22743  matring  22791  matassa  22792  ofco2  22799  mdetunilem1  22960  mdetunilem9  22968  mdetuni0  22969  mdetmul  22971  gsummatr01lem3  23005  iinopn  23253  subbascn  23605  nrmsep2  23707  isnrm3  23710  regsep2  23727  dnsconst  23729  dfconn2  23770  1stcelcls  23813  nllyidm  23841  dislly  23849  upxp  23975  fbasne0  24182  filss  24205  infil  24215  fsubbas  24219  filssufilg  24263  tmdcn2  24441  psmettri  24663  isxmet2d  24679  xmettri  24703  xmetres2  24713  bldisj  24750  blss2ps  24755  blss2  24756  xmstri2  24818  mstri2  24819  xmstri  24820  mstri  24821  xmstri3  24822  mstri3  24823  msrtri  24824  comet  24865  stdbdbl  24869  met2ndci  24874  ngprcan  24962  ngplcan  24963  ngpsubcan  24966  nmtri2  24979  nrgdsdi  25017  nrgdsdir  25018  nlmdsdi  25033  nlmdsdir  25034  blcvx  25150  icccmplem2  25176  pi1grplem  25403  pi1cof  25413  clmpm1dir  25457  cvsdiv  25486  cvsdivcl  25487  cphdivcl  25536  cphsubdir  25562  cphsubdi  25563  cphassr  25566  bcthlem5  25682  rrxcph  25746  volfiniun  25901  volcn  25960  itg1val2  26038  dvconst  26270  dvlip  26346  dvfsumlem4  26382  ftc1a  26390  ulmval  26740  ulmdvlem3  26762  ang180  27175  cvxcl  27345  scvxcvx  27346  sgmmul  27561  logexprlim  27585  dchrabl  27614  nosupbnd1  28104  noinfbnd1lem5  28117  noinfbnd1  28119  sltsss1  28184  motgrp  29039  iscgra1  29350  cgrane1  29352  cgrane2  29353  cgrahl1  29356  cgrahl2  29357  cgracgr  29358  cgratr  29363  cgrabtwn  29367  dfcgra2  29371  sacgr  29372  angmgmaddcl  29424  f1otrge  29482  colinearalglem1  29517  colinearalg  29521  axcgrtr  29526  axlowdimlem16  29568  axeuclidlem  29573  axcontlem7  29581  eengtrkg  29597  eengtrkge  29598  nbfusgrlevtxm2  29992  lfgriswlk  30304  upgrwlkdvde  30356  wwlknbp1  30466  usgrwwlks2on  30580  erclwwlktr  30646  erclwwlkntr  30695  frgr2wwlkeqm  30965  numclwwlk1lem2f  30989  numclwwlk5  31022  friendship  31033  grpodivdiv  31175  grpomuldivass  31176  ablodivdiv4  31189  ablonnncan1  31192  nvmdi  31283  dipassr  31481  archiabllem2c  33832  dvrcan5  33872  rloccring  33908  reofld  33988  eqgvscpbl  33995  qusvsval  33997  quslmod  34003  quslmhm  34004  dvdsruasso2  34025  ssmxidl  34083  ply1degltlss  34211  r1plmhm  34224  drgextlsp  34309  ccfldsrarelvec  34386  constrconj  34460  constrfin  34461  constrelextdg2  34462  pstmfval  34611  tpr2rico  34627  qqhval2lem  34696  qqhvq  34702  issiga  34827  measdivcst  34940  measdivcstALTV  34941  carsggect  35033  signsply0  35263  tgoldbachgtd  35374  bnj149  35588  bnj1118  35697  bnj1128  35703  erdszelem9  36144  resconn  36191  cvmseu  36221  cvmlift2lem12  36259  ex-sategoelel  36366  elmrsubrn  36465  mclsind  36515  r1peuqusdeg1  36588  cgrid2  36959  segconeu  36967  btwncomim  36969  btwnswapid  36973  cgrxfr  37011  btwnxfr  37012  colineardim1  37017  brofs2  37033  brifs2  37034  idinside  37040  endofsegid  37041  btwnconn1lem7  37049  btwnconn1lem11  37053  btwnconn1  37057  segcon2  37061  seglemin  37069  segletr  37070  btwnsegle  37073  colinbtwnle  37074  broutsideof2  37078  broutsideof3  37082  outsidele  37088  fvray  37097  fvline  37100  linerflx1  37105  ellines  37108  ivthALT  37314  weiunpo  37444  poimirlem32  38775  ftc1anc  38824  sdclem1  38880  sstotbnd2  38911  zerdivemp1x  39084  isdrngo2  39095  iscringd  39135  lsmsat  40268  lfladdcl  40331  lflnegcl  40335  lflvscl  40337  lshpkrlem4  40373  lshpkrlem6  40375  ldualgrplem  40405  lduallmodlem  40412  latmassOLD  40489  latm12  40490  latm32  40491  latmrot  40492  latmmdiN  40494  latmmdir  40495  omlfh1N  40518  omlfh3N  40519  cvlexchb1  40590  cvlexch3  40592  cvlexch4N  40593  cvlatexchb1  40594  cvlsupr2  40603  hlatjass  40630  hlatj12  40631  hlatj32  40632  cvratlem  40681  cvrat  40682  atcvrj0  40688  cvrat2  40689  atltcvr  40695  atexchltN  40701  cvrat3  40702  cvrat4  40703  3dimlem3  40721  3dimlem3OLDN  40722  3at  40750  2atneat  40775  llncmp  40782  2at0mat0  40785  2atmat0  40786  lplnnle2at  40801  llncvrlpln  40818  lplncmp  40822  lplnexllnN  40824  2llnjaN  40826  4atlem11  40869  lplncvrlvol  40876  lvolcmp  40877  2atm2atN  41045  elpaddatriN  41063  paddasslem9  41088  paddass  41098  padd12N  41099  paddssw2  41104  paddss  41105  pmodlem2  41107  pmodN  41110  pmapjlln1  41115  atmod1i1  41117  atmod1i2  41119  pexmidlem2N  41231  pexmidlem6N  41235  pl42N  41243  lhpm0atN  41289  lautlt  41351  lautcvr  41352  lautj  41353  lautm  41354  ltrneq2  41408  cdlemc3  41453  cdlemc4  41454  cdlemd1  41458  cdleme1b  41486  cdleme1  41487  cdleme2  41488  cdleme3e  41492  cdlemefr27cl  41663  cdlemefs27cl  41673  cdleme42mN  41747  cdlemftr2  41826  trljco  42000  tgrpgrplem  42009  tendoplass  42043  tendodi1  42044  tendodi2  42045  cdlemk36  42173  erngdvlem3  42250  erngdvlem3-rN  42258  tendospdi1  42280  dvalveclem  42285  dialss  42306  dvhvaddass  42357  dvhopvsca  42362  dvhlveclem  42368  diblss  42430  diclss  42453  dihmeetlem12N  42578  dihmeetlem15N  42581  dihmeetlem16N  42582  dihmeetlem17N  42583  dihmeetlem18N  42584  dihmeetlem19N  42585  dvh4dimN  42707  lpolvN  42746  lclkr  42793  lclkrs  42799  lcfr  42845  aks6d1c1  43369  irrapxlem6  44038  jm2.26lem3  44212  dgrsub2  44340  mpaadgr  44359  mendring  44393  mendlmod  44394  mendassa  44395  nnoeomeqom  44517  omabs2  44537  relexpmulg  44913  iunrelexpmin2  44915  relexpxpmin  44920  neicvgel1  45322  fmuldfeq  46810  stoweidlem43  47268  stoweidlem52  47277  stoweidlem53  47278  stoweidlem56  47281  stoweidlem57  47282  issmfle  47970  issmfgt  47981  issmfge  47995  submodaddmod  48632  fmtnoprmfac1  48865  fmtnoprmfac2  48867  clnbgredg  49153  cycl3grtrilem  49259  grlimprclnbgr  49309  grlimprclnbgredg  49310  upgrwlkupwlk  49453  copissgrp  49480  cznrng  49573  funcringcsetcALTV2lem9  49610  funcringcsetclem9ALTV  49633  idomcanl  49659  linccl  49741  lincext1  49781  lincext3  49783  lincresunit2  49805  line  50060  rrxline  50062  itsclc0yqsol  50091  resipos  50304  topdlat  50333  catprs  50340  endmndlem  50344  idmon  50349  idepi  50350  thincmon  50783  thincepi  50784  grptcmon  50946  grptcepi  50947  nellindf  51282