Theorem simpr1 1196

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 1190	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

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

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 1089

This theorem is referenced by:  simpr11  1259  simpr21  1262  simpr31  1265  simp1r1  1271  simp2r1  1277  simp3r1  1283  3anandis  1474  fpr2g  7166  isopolem  7300  fr3nr  7726  sexp3  8103  suppfnss  8139  frrlem4  8239  frrlem8  8243  dif1en  9096  frfi  9195  intrnfi  9329  iinfi  9330  eqsup  9369  fisupcl  9383  cnfcomlem  9620  ttrclss  9641  ackbij1lem15  10155  fpwwe2lem4  10557  dedekindle  11310  ico0  13344  elioc2  13362  elico2  13363  elicc2  13364  iccsplit  13438  fseq1p1m1  13552  elfz0ubfz0  13586  hashtpg  14447  hash7g  14448  swrdsbslen  14627  ccatswrd  14631  wwlktovf1  14919  tanadd  16134  dvds2ln  16258  qredeq  16626  ressress  17217  mreexexlem4d  17613  mreexexd  17614  0catg  17654  2oppccomf  17691  issubc3  17816  fthmon  17896  fuccocl  17934  fucidcl  17935  invfuc  17944  initoeu2lem0  17980  initoeu2lem1  17981  curf2cl  18197  yonedalem4c  18243  yonedalem3  18246  pospo  18309  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  18701  prdsmndd  18738  imasmnd2  18742  mndissubm  18775  frmdmnd  18827  grpsubrcan  18997  grpsubadd  19004  grpsubsub  19005  grpaddsubass  19006  grpsubsub4  19009  grpnnncan2  19013  imasgrp2  19031  mulgnndir  19079  mulgnn0dir  19080  mulgdir  19082  mulgnnass  19085  mulgnn0ass  19086  mulgass  19087  mulgsubdir  19090  pwsmulg  19095  issubg2  19117  eqgval  19152  qusgrp  19161  kerf1ghm  19222  galcan  19279  gacan  19280  oppgmnd  19329  pmtrprfv  19428  pmtr3ncom  19450  psgnunilem3  19471  cmn32  19775  cmn12  19777  abladdsub  19787  ablsubaddsub  19789  mulgnn0di  19800  mulgdi  19801  mulgsubdi  19804  dprdss  20006  dprdz  20007  dprdf1o  20009  dprdsn  20013  dprd2da  20019  ablfac1b  20047  pgpfac1lem5  20056  prdsrngd  20157  imasrng  20158  srgbinomlem2  20208  srgbinom  20212  ringdilem  20230  prdsringd  20300  imasring  20310  opprrng  20325  mulgass3  20333  dvrass  20388  dvrdir  20392  subrgunit  20567  issubrg2  20569  abvdiv  20806  islss3  20954  prdslmodd  20964  islmhm2  21033  lspsolv  21141  islbs2  21152  islbs3  21153  lbsextlem4  21159  sralmod  21182  ipdir  21619  ipdi  21620  ipsubdir  21622  ipsubdi  21623  ipass  21625  ipassr  21626  ipassr2  21627  ocvlss  21652  psrlmod  21938  psrring  21948  psrassa  21951  ply1ass23l  22190  mamudm  22360  matring  22408  matassa  22409  ofco2  22416  mdetunilem1  22577  mdetunilem9  22585  mdetuni0  22586  mdetmul  22588  gsummatr01lem3  22622  iinopn  22867  subbascn  23219  nrmsep2  23321  isnrm3  23324  regsep2  23341  dnsconst  23343  dfconn2  23384  1stcelcls  23426  nllyidm  23454  dislly  23462  upxp  23588  fbasne0  23795  filss  23818  infil  23828  fsubbas  23832  filssufilg  23876  tmdcn2  24054  psmettri  24276  isxmet2d  24292  xmettri  24316  xmetres2  24326  bldisj  24363  blss2ps  24368  blss2  24369  xmstri2  24431  mstri2  24432  xmstri  24433  mstri  24434  xmstri3  24435  mstri3  24436  msrtri  24437  comet  24478  stdbdbl  24482  met2ndci  24487  ngprcan  24575  ngplcan  24576  ngpsubcan  24579  nmtri2  24592  nrgdsdi  24630  nrgdsdir  24631  nlmdsdi  24646  nlmdsdir  24647  blcvx  24763  icccmplem2  24789  pi1grplem  25016  pi1cof  25026  clmpm1dir  25070  cvsdiv  25099  cvsdivcl  25100  cphdivcl  25149  cphsubdir  25175  cphsubdi  25176  cphassr  25179  bcthlem5  25295  rrxcph  25359  volfiniun  25514  volcn  25573  itg1val2  25651  dvconst  25884  dvlip  25960  dvfsumlem4  25996  ftc1a  26004  ulmval  26345  ulmdvlem3  26367  ang180  26778  cvxcl  26948  scvxcvx  26949  sgmmul  27164  logexprlim  27188  dchrabl  27217  nosupbnd1  27678  noinfbnd1lem5  27691  noinfbnd1  27693  sltsss1  27757  motgrp  28611  iscgra1  28878  cgrane1  28880  cgrane2  28881  cgrahl1  28884  cgrahl2  28885  cgracgr  28886  cgratr  28891  cgrabtwn  28894  dfcgra2  28898  sacgr  28899  f1otrge  28940  colinearalglem1  28975  colinearalg  28979  axcgrtr  28984  axlowdimlem16  29026  axeuclidlem  29031  axcontlem7  29039  eengtrkg  29055  eengtrkge  29056  nbfusgrlevtxm2  29447  lfgriswlk  29755  upgrwlkdvde  29805  wwlknbp1  29912  usgrwwlks2on  30026  erclwwlktr  30092  erclwwlkntr  30141  frgr2wwlkeqm  30401  numclwwlk1lem2f  30425  numclwwlk5  30458  friendship  30469  grpodivdiv  30611  grpomuldivass  30612  ablodivdiv4  30625  ablonnncan1  30628  nvmdi  30719  dipassr  30917  archiabllem2c  33256  dvrcan5  33297  rloccring  33331  reofld  33403  eqgvscpbl  33410  qusvsval  33412  quslmod  33418  quslmhm  33419  dvdsruasso2  33446  prmidlc  33508  ssdifidl  33517  ssmxidl  33534  ply1degltlss  33656  r1plmhm  33670  drgextlsp  33738  ccfldsrarelvec  33815  constrconj  33889  constrfin  33890  constrelextdg2  33891  pstmfval  34040  tpr2rico  34056  qqhval2lem  34125  qqhvq  34131  issiga  34256  measdivcst  34368  measdivcstALTV  34369  carsggect  34462  signsply0  34695  tgoldbachgtd  34806  bnj149  35017  bnj1118  35126  bnj1128  35132  erdszelem9  35381  resconn  35428  cvmseu  35458  cvmlift2lem12  35496  ex-sategoelel  35603  elmrsubrn  35702  mclsind  35752  r1peuqusdeg1  35825  cgrid2  36185  segconeu  36193  btwncomim  36195  btwnswapid  36199  cgrxfr  36237  btwnxfr  36238  colineardim1  36243  brofs2  36259  brifs2  36260  idinside  36266  endofsegid  36267  btwnconn1lem7  36275  btwnconn1lem11  36279  btwnconn1  36283  segcon2  36287  seglemin  36295  segletr  36296  btwnsegle  36299  colinbtwnle  36300  broutsideof2  36304  broutsideof3  36308  outsidele  36314  fvray  36323  fvline  36326  linerflx1  36331  ellines  36334  ivthALT  36517  weiunpo  36647  poimirlem32  37973  ftc1anc  38022  sdclem1  38064  sstotbnd2  38095  zerdivemp1x  38268  isdrngo2  38279  iscringd  38319  lsmsat  39454  lfladdcl  39517  lflnegcl  39521  lflvscl  39523  lshpkrlem4  39559  lshpkrlem6  39561  ldualgrplem  39591  lduallmodlem  39598  latmassOLD  39675  latm12  39676  latm32  39677  latmrot  39678  latmmdiN  39680  latmmdir  39681  omlfh1N  39704  omlfh3N  39705  cvlexchb1  39776  cvlexch3  39778  cvlexch4N  39779  cvlatexchb1  39780  cvlsupr2  39789  hlatjass  39816  hlatj12  39817  hlatj32  39818  cvratlem  39867  cvrat  39868  atcvrj0  39874  cvrat2  39875  atltcvr  39881  atexchltN  39887  cvrat3  39888  cvrat4  39889  3dimlem3  39907  3dimlem3OLDN  39908  3at  39936  2atneat  39961  llncmp  39968  2at0mat0  39971  2atmat0  39972  lplnnle2at  39987  llncvrlpln  40004  lplncmp  40008  lplnexllnN  40010  2llnjaN  40012  4atlem11  40055  lplncvrlvol  40062  lvolcmp  40063  2atm2atN  40231  elpaddatriN  40249  paddasslem9  40274  paddass  40284  padd12N  40285  paddssw2  40290  paddss  40291  pmodlem2  40293  pmodN  40296  pmapjlln1  40301  atmod1i1  40303  atmod1i2  40305  pexmidlem2N  40417  pexmidlem6N  40421  pl42N  40429  lhpm0atN  40475  lautlt  40537  lautcvr  40538  lautj  40539  lautm  40540  ltrneq2  40594  cdlemc3  40639  cdlemc4  40640  cdlemd1  40644  cdleme1b  40672  cdleme1  40673  cdleme2  40674  cdleme3e  40678  cdlemefr27cl  40849  cdlemefs27cl  40859  cdleme42mN  40933  cdlemftr2  41012  trljco  41186  tgrpgrplem  41195  tendoplass  41229  tendodi1  41230  tendodi2  41231  cdlemk36  41359  erngdvlem3  41436  erngdvlem3-rN  41444  tendospdi1  41466  dvalveclem  41471  dialss  41492  dvhvaddass  41543  dvhopvsca  41548  dvhlveclem  41554  diblss  41616  diclss  41639  dihmeetlem12N  41764  dihmeetlem15N  41767  dihmeetlem16N  41768  dihmeetlem17N  41769  dihmeetlem18N  41770  dihmeetlem19N  41771  dvh4dimN  41893  lpolvN  41932  lclkr  41979  lclkrs  41985  lcfr  42031  aks6d1c1  42555  irrapxlem6  43255  jm2.26lem3  43429  dgrsub2  43563  mpaadgr  43582  mendring  43616  mendlmod  43617  mendassa  43618  nnoeomeqom  43740  omabs2  43760  relexpmulg  44137  iunrelexpmin2  44139  relexpxpmin  44144  neicvgel1  44546  fmuldfeq  46013  stoweidlem43  46471  stoweidlem52  46480  stoweidlem53  46481  stoweidlem56  46484  stoweidlem57  46485  issmfle  47173  issmfgt  47184  issmfge  47198  submodaddmod  47795  fmtnoprmfac1  48028  fmtnoprmfac2  48030  clnbgredg  48316  cycl3grtrilem  48422  grlimprclnbgr  48472  grlimprclnbgredg  48473  upgrwlkupwlk  48616  copissgrp  48644  cznrng  48737  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797  linccl  48890  lincext1  48930  lincext3  48932  lincresunit2  48954  line  49208  rrxline  49210  itsclc0yqsol  49240  resipos  49450  topdlat  49479  catprs  49486  endmndlem  49490  idmon  49495  idepi  49496  thincmon  49908  thincepi  49909  grptcmon  50068  grptcepi  50069