Theorem simpr1 1195

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpr11  1258  simpr21  1261  simpr31  1264  simp1r1  1270  simp2r1  1276  simp3r1  1282  3anandis  1473  fpr2g  7188  isopolem  7323  fr3nr  7751  sexp3  8135  suppfnss  8171  frrlem4  8271  frrlem8  8275  dif1en  9130  frfi  9239  intrnfi  9374  iinfi  9375  eqsup  9414  fisupcl  9428  cnfcomlem  9659  ttrclss  9680  ackbij1lem15  10193  fpwwe2lem4  10594  dedekindle  11345  ico0  13359  elioc2  13377  elico2  13378  elicc2  13379  iccsplit  13453  fseq1p1m1  13566  elfz0ubfz0  13600  hashtpg  14457  hash7g  14458  swrdsbslen  14636  ccatswrd  14640  wwlktovf1  14930  tanadd  16142  dvds2ln  16266  qredeq  16634  ressress  17224  mreexexlem4d  17615  mreexexd  17616  0catg  17656  2oppccomf  17693  issubc3  17818  fthmon  17898  fuccocl  17936  fucidcl  17937  invfuc  17946  initoeu2lem0  17982  initoeu2lem1  17983  curf2cl  18199  yonedalem4c  18245  yonedalem3  18248  pospo  18311  latjle12  18416  latjlej1  18419  latnlej2  18425  latlem12  18432  latmlem1  18435  latledi  18443  latmlej11  18444  latjass  18449  latj12  18450  latj32  18451  latj13  18452  latj31  18453  latjrot  18454  latjjdi  18457  latjjdir  18458  latdisdlem  18462  prdssgrpd  18667  prdsmndd  18704  imasmnd2  18708  mndissubm  18741  frmdmnd  18793  grpsubrcan  18960  grpsubadd  18967  grpsubsub  18968  grpaddsubass  18969  grpsubsub4  18972  grpnnncan2  18976  imasgrp2  18994  mulgnndir  19042  mulgnn0dir  19043  mulgdir  19045  mulgnnass  19048  mulgnn0ass  19049  mulgass  19050  mulgsubdir  19053  pwsmulg  19058  issubg2  19080  eqgval  19116  qusgrp  19125  kerf1ghm  19186  galcan  19243  gacan  19244  oppgmnd  19293  pmtrprfv  19390  pmtr3ncom  19412  psgnunilem3  19433  cmn32  19737  cmn12  19739  abladdsub  19749  ablsubaddsub  19751  mulgnn0di  19762  mulgdi  19763  mulgsubdi  19766  dprdss  19968  dprdz  19969  dprdf1o  19971  dprdsn  19975  dprd2da  19981  ablfac1b  20009  pgpfac1lem5  20018  prdsrngd  20092  imasrng  20093  srgbinomlem2  20143  srgbinom  20147  ringdilem  20165  prdsringd  20237  imasring  20246  opprrng  20261  mulgass3  20269  dvrass  20324  dvrdir  20328  subrgunit  20506  issubrg2  20508  abvdiv  20745  islss3  20872  prdslmodd  20882  islmhm2  20952  lspsolv  21060  islbs2  21071  islbs3  21072  lbsextlem4  21078  sralmod  21101  ipdir  21555  ipdi  21556  ipsubdir  21558  ipsubdi  21559  ipass  21561  ipassr  21562  ipassr2  21563  ocvlss  21588  sraassaOLD  21786  psrgrpOLD  21873  psrlmod  21876  psrring  21886  psrassa  21889  ply1ass23l  22118  mamudm  22289  matring  22337  matassa  22338  ofco2  22345  mdetunilem1  22506  mdetunilem9  22514  mdetuni0  22515  mdetmul  22517  gsummatr01lem3  22551  iinopn  22796  subbascn  23148  nrmsep2  23250  isnrm3  23253  regsep2  23270  dnsconst  23272  dfconn2  23313  1stcelcls  23355  nllyidm  23383  dislly  23391  upxp  23517  fbasne0  23724  filss  23747  infil  23757  fsubbas  23761  filssufilg  23805  tmdcn2  23983  psmettri  24206  isxmet2d  24222  xmettri  24246  xmetres2  24256  bldisj  24293  blss2ps  24298  blss2  24299  xmstri2  24361  mstri2  24362  xmstri  24363  mstri  24364  xmstri3  24365  mstri3  24366  msrtri  24367  comet  24408  stdbdbl  24412  met2ndci  24417  ngprcan  24505  ngplcan  24506  ngpsubcan  24509  nmtri2  24522  nrgdsdi  24560  nrgdsdir  24561  nlmdsdi  24576  nlmdsdir  24577  blcvx  24693  icccmplem2  24719  pi1grplem  24956  pi1cof  24966  clmpm1dir  25010  cvsdiv  25039  cvsdivcl  25040  cphdivcl  25089  cphsubdir  25115  cphsubdi  25116  cphassr  25119  bcthlem5  25235  rrxcph  25299  volfiniun  25455  volcn  25514  itg1val2  25592  dvconst  25825  dvlip  25905  dvfsumlem4  25943  ftc1a  25951  ulmval  26296  ulmdvlem3  26318  ang180  26731  cvxcl  26902  scvxcvx  26903  sgmmul  27119  logexprlim  27143  dchrabl  27172  nosupbnd1  27633  noinfbnd1lem5  27646  noinfbnd1  27648  ssltss1  27707  motgrp  28477  iscgra1  28744  cgrane1  28746  cgrane2  28747  cgrahl1  28750  cgrahl2  28751  cgracgr  28752  cgratr  28757  cgrabtwn  28760  dfcgra2  28764  sacgr  28765  f1otrge  28806  colinearalglem1  28840  colinearalg  28844  axcgrtr  28849  axlowdimlem16  28891  axeuclidlem  28896  axcontlem7  28904  eengtrkg  28920  eengtrkge  28921  nbfusgrlevtxm2  29312  lfgriswlk  29623  upgrwlkdvde  29674  wwlknbp1  29781  erclwwlktr  29958  erclwwlkntr  30007  frgr2wwlkeqm  30267  numclwwlk1lem2f  30291  numclwwlk5  30324  friendship  30335  grpodivdiv  30476  grpomuldivass  30477  ablodivdiv4  30490  ablonnncan1  30493  nvmdi  30584  dipassr  30782  archiabllem2c  33156  dvrcan5  33194  rloccring  33228  reofld  33322  eqgvscpbl  33328  qusvsval  33330  quslmod  33336  quslmhm  33337  dvdsruasso2  33364  prmidlc  33426  ssdifidl  33435  ssmxidl  33452  ply1degltlss  33569  r1plmhm  33582  drgextlsp  33596  ccfldsrarelvec  33673  constrconj  33742  constrfin  33743  constrelextdg2  33744  pstmfval  33893  tpr2rico  33909  qqhval2lem  33978  qqhvq  33984  issiga  34109  measdivcst  34221  measdivcstALTV  34222  carsggect  34316  signsply0  34549  tgoldbachgtd  34660  bnj149  34872  bnj1118  34981  bnj1128  34987  erdszelem9  35193  resconn  35240  cvmseu  35270  cvmlift2lem12  35308  ex-sategoelel  35415  elmrsubrn  35514  mclsind  35564  r1peuqusdeg1  35637  cgrid2  35998  segconeu  36006  btwncomim  36008  btwnswapid  36012  cgrxfr  36050  btwnxfr  36051  colineardim1  36056  brofs2  36072  brifs2  36073  idinside  36079  endofsegid  36080  btwnconn1lem7  36088  btwnconn1lem11  36092  btwnconn1  36096  segcon2  36100  seglemin  36108  segletr  36109  btwnsegle  36112  colinbtwnle  36113  broutsideof2  36117  broutsideof3  36121  outsidele  36127  fvray  36136  fvline  36139  linerflx1  36144  ellines  36147  ivthALT  36330  weiunpo  36460  poimirlem32  37653  ftc1anc  37702  sdclem1  37744  sstotbnd2  37775  zerdivemp1x  37948  isdrngo2  37959  iscringd  37999  lsmsat  39008  lfladdcl  39071  lflnegcl  39075  lflvscl  39077  lshpkrlem4  39113  lshpkrlem6  39115  ldualgrplem  39145  lduallmodlem  39152  latmassOLD  39229  latm12  39230  latm32  39231  latmrot  39232  latmmdiN  39234  latmmdir  39235  omlfh1N  39258  omlfh3N  39259  cvlexchb1  39330  cvlexch3  39332  cvlexch4N  39333  cvlatexchb1  39334  cvlsupr2  39343  hlatjass  39370  hlatj12  39371  hlatj32  39372  cvratlem  39422  cvrat  39423  atcvrj0  39429  cvrat2  39430  atltcvr  39436  atexchltN  39442  cvrat3  39443  cvrat4  39444  3dimlem3  39462  3dimlem3OLDN  39463  3at  39491  2atneat  39516  llncmp  39523  2at0mat0  39526  2atmat0  39527  lplnnle2at  39542  llncvrlpln  39559  lplncmp  39563  lplnexllnN  39565  2llnjaN  39567  4atlem11  39610  lplncvrlvol  39617  lvolcmp  39618  2atm2atN  39786  elpaddatriN  39804  paddasslem9  39829  paddass  39839  padd12N  39840  paddssw2  39845  paddss  39846  pmodlem2  39848  pmodN  39851  pmapjlln1  39856  atmod1i1  39858  atmod1i2  39860  pexmidlem2N  39972  pexmidlem6N  39976  pl42N  39984  lhpm0atN  40030  lautlt  40092  lautcvr  40093  lautj  40094  lautm  40095  ltrneq2  40149  cdlemc3  40194  cdlemc4  40195  cdlemd1  40199  cdleme1b  40227  cdleme1  40228  cdleme2  40229  cdleme3e  40233  cdlemefr27cl  40404  cdlemefs27cl  40414  cdleme42mN  40488  cdlemftr2  40567  trljco  40741  tgrpgrplem  40750  tendoplass  40784  tendodi1  40785  tendodi2  40786  cdlemk36  40914  erngdvlem3  40991  erngdvlem3-rN  40999  tendospdi1  41021  dvalveclem  41026  dialss  41047  dvhvaddass  41098  dvhopvsca  41103  dvhlveclem  41109  diblss  41171  diclss  41194  dihmeetlem12N  41319  dihmeetlem15N  41322  dihmeetlem16N  41323  dihmeetlem17N  41324  dihmeetlem18N  41325  dihmeetlem19N  41326  dvh4dimN  41448  lpolvN  41487  lclkr  41534  lclkrs  41540  lcfr  41586  aks6d1c1  42111  irrapxlem6  42822  jm2.26lem3  42997  dgrsub2  43131  mpaadgr  43150  mendring  43184  mendlmod  43185  mendassa  43186  nnoeomeqom  43308  omabs2  43328  relexpmulg  43706  iunrelexpmin2  43708  relexpxpmin  43713  neicvgel1  44115  fmuldfeq  45588  stoweidlem43  46048  stoweidlem52  46057  stoweidlem53  46058  stoweidlem56  46061  stoweidlem57  46062  issmfle  46750  issmfgt  46761  issmfge  46775  submodaddmod  47346  fmtnoprmfac1  47570  fmtnoprmfac2  47572  clnbgredg  47844  cycl3grtrilem  47949  grlimgrtrilem1  47997  upgrwlkupwlk  48132  copissgrp  48160  cznrng  48253  funcringcsetcALTV2lem9  48290  funcringcsetclem9ALTV  48313  linccl  48407  lincext1  48447  lincext3  48449  lincresunit2  48471  line  48725  rrxline  48727  itsclc0yqsol  48757  resipos  48967  topdlat  48996  catprs  49004  endmndlem  49008  idmon  49013  idepi  49014  thincmon  49426  thincepi  49427  grptcmon  49586  grptcepi  49587