Theorem simpr1 1190

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr11  1253  simpr21  1256  simpr31  1259  simp1r1  1265  simp2r1  1271  simp3r1  1277  3anandis  1467  fpr2g  6974  isopolem  7098  fr3nr  7494  suppfnss  7855  frfi  8763  intrnfi  8880  iinfi  8881  eqsup  8920  fisupcl  8933  cnfcomlem  9162  ackbij1lem15  9656  fpwwe2lem5  10056  dedekindle  10804  ico0  12785  elioc2  12800  elico2  12801  elicc2  12802  iccsplit  12872  fseq1p1m1  12982  elfz0ubfz0  13012  hashtpg  13844  swrdsbslen  14026  ccatswrd  14030  wwlktovf1  14321  tanadd  15520  dvds2ln  15642  qredeq  16001  ressress  16562  mreexexlem4d  16918  mreexexd  16919  0catg  16958  2oppccomf  16995  issubc3  17119  fthmon  17197  fuccocl  17234  fucidcl  17235  invfuc  17244  initoeu2lem0  17273  initoeu2lem1  17274  curf2cl  17481  yonedalem4c  17527  yonedalem3  17530  pospo  17583  latjle12  17672  latjlej1  17675  latnlej2  17681  latlem12  17688  latmlem1  17691  latledi  17699  latmlej11  17700  latjass  17705  latj12  17706  latj32  17707  latj13  17708  latj31  17709  latjrot  17710  latjjdi  17713  latjjdir  17714  latdisdlem  17799  prdsmndd  17944  imasmnd2  17948  mndissubm  17972  frmdmnd  18024  grpsubrcan  18180  grpsubadd  18187  grpsubsub  18188  grpaddsubass  18189  grpsubsub4  18192  grpnnncan2  18196  imasgrp2  18214  mulgnndir  18256  mulgnn0dir  18257  mulgdir  18259  mulgnnass  18262  mulgnn0ass  18263  mulgass  18264  mulgsubdir  18267  pwsmulg  18272  issubg2  18294  eqgval  18329  qusgrp  18335  galcan  18434  gacan  18435  oppgmnd  18482  pmtrprfv  18581  pmtr3ncom  18603  psgnunilem3  18624  cmn32  18925  cmn12  18927  abladdsub  18935  mulgnn0di  18946  mulgdi  18947  mulgsubdi  18950  dprdss  19151  dprdz  19152  dprdf1o  19154  dprdsn  19158  dprd2da  19164  ablfac1b  19192  pgpfac1lem5  19201  srgbinomlem2  19291  srgbinom  19295  ringi  19310  prdsringd  19362  imasring  19369  opprring  19381  mulgass3  19387  dvrass  19440  kerf1ghm  19497  kerf1hrmOLD  19498  subrgunit  19553  issubrg2  19555  abvdiv  19608  islss3  19731  prdslmodd  19741  islmhm2  19810  lspsolv  19915  islbs2  19926  islbs3  19927  lbsextlem4  19933  sralmod  19959  sraassa  20099  psrbaglecl  20149  psrbagcon  20151  psrgrp  20178  psrlmod  20181  psrring  20191  psrassa  20194  ipdir  20783  ipdi  20784  ipsubdir  20786  ipsubdi  20787  ipass  20789  ipassr  20790  ipassr2  20791  ocvlss  20816  mamudm  20999  matring  21052  matassa  21053  ofco2  21060  mdetunilem1  21221  mdetunilem9  21229  mdetuni0  21230  mdetmul  21232  gsummatr01lem3  21266  iinopn  21510  subbascn  21862  nrmsep2  21964  isnrm3  21967  regsep2  21984  dnsconst  21986  dfconn2  22027  1stcelcls  22069  nllyidm  22097  dislly  22105  upxp  22231  fbasne0  22438  filss  22461  infil  22471  fsubbas  22475  filssufilg  22519  tmdcn2  22697  psmettri  22921  isxmet2d  22937  xmettri  22961  xmetres2  22971  bldisj  23008  blss2ps  23013  blss2  23014  xmstri2  23076  mstri2  23077  xmstri  23078  mstri  23079  xmstri3  23080  mstri3  23081  msrtri  23082  comet  23123  stdbdbl  23127  met2ndci  23132  ngprcan  23219  ngplcan  23220  ngpsubcan  23223  nmtri2  23236  nrgdsdi  23274  nrgdsdir  23275  nlmdsdi  23290  nlmdsdir  23291  blcvx  23406  icccmplem2  23431  pi1grplem  23653  pi1cof  23663  clmpm1dir  23707  cvsdiv  23736  cvsdivcl  23737  cphdivcl  23786  cphsubdir  23812  cphsubdi  23813  cphassr  23816  bcthlem5  23931  rrxcph  23995  volfiniun  24148  volcn  24207  itg1val2  24285  dvconst  24514  dvlip  24590  dvfsumlem4  24626  ftc1a  24634  ulmval  24968  ulmdvlem3  24990  ang180  25392  cvxcl  25562  scvxcvx  25563  sgmmul  25777  logexprlim  25801  dchrabl  25830  motgrp  26329  iscgra1  26596  cgrane1  26598  cgrane2  26599  cgrahl1  26602  cgrahl2  26603  cgracgr  26604  cgratr  26609  cgrabtwn  26612  dfcgra2  26616  sacgr  26617  f1otrge  26658  colinearalglem1  26692  colinearalg  26696  axcgrtr  26701  axlowdimlem16  26743  axeuclidlem  26748  axcontlem7  26756  eengtrkg  26772  eengtrkge  26773  nbfusgrlevtxm2  27160  lfgriswlk  27470  upgrwlkdvde  27518  wwlknbp1  27622  erclwwlktr  27800  erclwwlkntr  27850  frgr2wwlkeqm  28110  numclwwlk1lem2f  28134  numclwwlk5  28167  friendship  28178  grpodivdiv  28317  grpomuldivass  28318  ablodivdiv4  28331  ablonnncan1  28334  nvmdi  28425  dipassr  28623  archiabllem2c  30824  dvrdir  30861  dvrcan5  30864  reofld  30913  eqgvscpbl  30919  qusscaval  30921  quslmod  30923  quslmhm  30924  prmidlc  30964  ssmxidl  30979  drgextlsp  30996  ccfldsrarelvec  31056  pstmfval  31136  tpr2rico  31155  qqhval2lem  31222  qqhvq  31228  issiga  31371  measdivcst  31483  measdivcstALTV  31484  carsggect  31576  signsply0  31821  tgoldbachgtd  31933  bnj149  32147  bnj1118  32256  bnj1128  32262  erdszelem9  32446  resconn  32493  cvmseu  32523  cvmlift2lem12  32561  ex-sategoelel  32668  elmrsubrn  32767  mclsind  32817  frrlem4  33126  frrlem8  33130  noprefixmo  33202  nosupbnd1  33214  ssltss1  33257  cgrid2  33464  segconeu  33472  btwncomim  33474  btwnswapid  33478  cgrxfr  33516  btwnxfr  33517  colineardim1  33522  brofs2  33538  brifs2  33539  idinside  33545  endofsegid  33546  btwnconn1lem7  33554  btwnconn1lem11  33558  btwnconn1  33562  segcon2  33566  seglemin  33574  segletr  33575  btwnsegle  33578  colinbtwnle  33579  broutsideof2  33583  broutsideof3  33587  outsidele  33593  fvray  33602  fvline  33605  linerflx1  33610  ellines  33613  ivthALT  33683  poimirlem32  34939  ftc1anc  34990  sdclem1  35033  sstotbnd2  35067  zerdivemp1x  35240  isdrngo2  35251  iscringd  35291  lsmsat  36159  lfladdcl  36222  lflnegcl  36226  lflvscl  36228  lshpkrlem4  36264  lshpkrlem6  36266  ldualgrplem  36296  lduallmodlem  36303  latmassOLD  36380  latm12  36381  latm32  36382  latmrot  36383  latmmdiN  36385  latmmdir  36386  omlfh1N  36409  omlfh3N  36410  cvlexchb1  36481  cvlexch3  36483  cvlexch4N  36484  cvlatexchb1  36485  cvlsupr2  36494  hlatjass  36521  hlatj12  36522  hlatj32  36523  cvratlem  36572  cvrat  36573  atcvrj0  36579  cvrat2  36580  atltcvr  36586  atexchltN  36592  cvrat3  36593  cvrat4  36594  3dimlem3  36612  3dimlem3OLDN  36613  3at  36641  2atneat  36666  llncmp  36673  2at0mat0  36676  2atmat0  36677  lplnnle2at  36692  llncvrlpln  36709  lplncmp  36713  lplnexllnN  36715  2llnjaN  36717  4atlem11  36760  lplncvrlvol  36767  lvolcmp  36768  2atm2atN  36936  elpaddatriN  36954  paddasslem9  36979  paddass  36989  padd12N  36990  paddssw2  36995  paddss  36996  pmodlem2  36998  pmodN  37001  pmapjlln1  37006  atmod1i1  37008  atmod1i2  37010  pexmidlem2N  37122  pexmidlem6N  37126  pl42N  37134  lhpm0atN  37180  lautlt  37242  lautcvr  37243  lautj  37244  lautm  37245  ltrneq2  37299  cdlemc3  37344  cdlemc4  37345  cdlemd1  37349  cdleme1b  37377  cdleme1  37378  cdleme2  37379  cdleme3e  37383  cdlemefr27cl  37554  cdlemefs27cl  37564  cdleme42mN  37638  cdlemftr2  37717  trljco  37891  tgrpgrplem  37900  tendoplass  37934  tendodi1  37935  tendodi2  37936  cdlemk36  38064  erngdvlem3  38141  erngdvlem3-rN  38149  tendospdi1  38171  dvalveclem  38176  dialss  38197  dvhvaddass  38248  dvhopvsca  38253  dvhlveclem  38259  diblss  38321  diclss  38344  dihmeetlem12N  38469  dihmeetlem15N  38472  dihmeetlem16N  38473  dihmeetlem17N  38474  dihmeetlem18N  38475  dihmeetlem19N  38476  dvh4dimN  38598  lpolvN  38637  lclkr  38684  lclkrs  38690  lcfr  38736  irrapxlem6  39473  jm2.26lem3  39647  dgrsub2  39784  mpaadgr  39803  mendring  39841  mendlmod  39842  mendassa  39843  relexpmulg  40104  iunrelexpmin2  40106  relexpxpmin  40111  neicvgel1  40518  fmuldfeq  41913  stoweidlem43  42377  stoweidlem52  42386  stoweidlem53  42387  stoweidlem56  42390  stoweidlem57  42391  issmfle  43071  issmfgt  43082  issmfge  43095  fmtnoprmfac1  43776  fmtnoprmfac2  43778  upgrwlkupwlk  44064  copissgrp  44124  cznrng  44275  funcringcsetcALTV2lem9  44364  funcringcsetclem9ALTV  44387  ply1ass23l  44485  linccl  44518  lincext1  44558  lincext3  44560  lincresunit2  44582  line  44768  rrxline  44770  itsclc0yqsol  44800