Theorem simpr1 1193

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 1187	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  1256  simpr21  1259  simpr31  1262  simp1r1  1268  simp2r1  1274  simp3r1  1280  3anandis  1470  fpr2g  7230  isopolem  7364  fr3nr  7790  sexp3  8176  suppfnss  8212  frrlem4  8312  frrlem8  8316  dif1en  9198  frfi  9318  intrnfi  9453  iinfi  9454  eqsup  9493  fisupcl  9506  cnfcomlem  9736  ttrclss  9757  ackbij1lem15  10270  fpwwe2lem4  10671  dedekindle  11422  ico0  13429  elioc2  13446  elico2  13447  elicc2  13448  iccsplit  13521  fseq1p1m1  13634  elfz0ubfz0  13668  hashtpg  14520  hash7g  14521  swrdsbslen  14698  ccatswrd  14702  wwlktovf1  14992  tanadd  16199  dvds2ln  16322  qredeq  16690  ressress  17293  mreexexlem4d  17691  mreexexd  17692  0catg  17732  2oppccomf  17771  issubc3  17899  fthmon  17980  fuccocl  18020  fucidcl  18021  invfuc  18030  initoeu2lem0  18066  initoeu2lem1  18067  curf2cl  18287  yonedalem4c  18333  yonedalem3  18336  pospo  18402  latjle12  18507  latjlej1  18510  latnlej2  18516  latlem12  18523  latmlem1  18526  latledi  18534  latmlej11  18535  latjass  18540  latj12  18541  latj32  18542  latj13  18543  latj31  18544  latjrot  18545  latjjdi  18548  latjjdir  18549  latdisdlem  18553  prdssgrpd  18758  prdsmndd  18795  imasmnd2  18799  mndissubm  18832  frmdmnd  18884  grpsubrcan  19051  grpsubadd  19058  grpsubsub  19059  grpaddsubass  19060  grpsubsub4  19063  grpnnncan2  19067  imasgrp2  19085  mulgnndir  19133  mulgnn0dir  19134  mulgdir  19136  mulgnnass  19139  mulgnn0ass  19140  mulgass  19141  mulgsubdir  19144  pwsmulg  19149  issubg2  19171  eqgval  19207  qusgrp  19216  kerf1ghm  19277  galcan  19334  gacan  19335  oppgmnd  19387  pmtrprfv  19485  pmtr3ncom  19507  psgnunilem3  19528  cmn32  19832  cmn12  19834  abladdsub  19844  ablsubaddsub  19846  mulgnn0di  19857  mulgdi  19858  mulgsubdi  19861  dprdss  20063  dprdz  20064  dprdf1o  20066  dprdsn  20070  dprd2da  20076  ablfac1b  20104  pgpfac1lem5  20113  prdsrngd  20193  imasrng  20194  srgbinomlem2  20244  srgbinom  20248  ringdilem  20266  prdsringd  20334  imasring  20343  opprrng  20361  mulgass3  20369  dvrass  20424  dvrdir  20428  subrgunit  20606  issubrg2  20608  abvdiv  20846  islss3  20974  prdslmodd  20984  islmhm2  21054  lspsolv  21162  islbs2  21173  islbs3  21174  lbsextlem4  21180  sralmod  21211  ipdir  21674  ipdi  21675  ipsubdir  21677  ipsubdi  21678  ipass  21680  ipassr  21681  ipassr2  21682  ocvlss  21707  sraassaOLD  21907  psrgrpOLD  21994  psrlmod  21997  psrring  22007  psrassa  22010  ply1ass23l  22243  mamudm  22414  matring  22464  matassa  22465  ofco2  22472  mdetunilem1  22633  mdetunilem9  22641  mdetuni0  22642  mdetmul  22644  gsummatr01lem3  22678  iinopn  22923  subbascn  23277  nrmsep2  23379  isnrm3  23382  regsep2  23399  dnsconst  23401  dfconn2  23442  1stcelcls  23484  nllyidm  23512  dislly  23520  upxp  23646  fbasne0  23853  filss  23876  infil  23886  fsubbas  23890  filssufilg  23934  tmdcn2  24112  psmettri  24336  isxmet2d  24352  xmettri  24376  xmetres2  24386  bldisj  24423  blss2ps  24428  blss2  24429  xmstri2  24491  mstri2  24492  xmstri  24493  mstri  24494  xmstri3  24495  mstri3  24496  msrtri  24497  comet  24541  stdbdbl  24545  met2ndci  24550  ngprcan  24638  ngplcan  24639  ngpsubcan  24642  nmtri2  24655  nrgdsdi  24701  nrgdsdir  24702  nlmdsdi  24717  nlmdsdir  24718  blcvx  24833  icccmplem2  24858  pi1grplem  25095  pi1cof  25105  clmpm1dir  25149  cvsdiv  25178  cvsdivcl  25179  cphdivcl  25229  cphsubdir  25255  cphsubdi  25256  cphassr  25259  bcthlem5  25375  rrxcph  25439  volfiniun  25595  volcn  25654  itg1val2  25732  dvconst  25966  dvlip  26046  dvfsumlem4  26084  ftc1a  26092  ulmval  26437  ulmdvlem3  26459  ang180  26871  cvxcl  27042  scvxcvx  27043  sgmmul  27259  logexprlim  27283  dchrabl  27312  nosupbnd1  27773  noinfbnd1lem5  27786  noinfbnd1  27788  ssltss1  27847  motgrp  28565  iscgra1  28832  cgrane1  28834  cgrane2  28835  cgrahl1  28838  cgrahl2  28839  cgracgr  28840  cgratr  28845  cgrabtwn  28848  dfcgra2  28852  sacgr  28853  f1otrge  28894  colinearalglem1  28935  colinearalg  28939  axcgrtr  28944  axlowdimlem16  28986  axeuclidlem  28991  axcontlem7  28999  eengtrkg  29015  eengtrkge  29016  nbfusgrlevtxm2  29409  lfgriswlk  29720  upgrwlkdvde  29769  wwlknbp1  29873  erclwwlktr  30050  erclwwlkntr  30099  frgr2wwlkeqm  30359  numclwwlk1lem2f  30383  numclwwlk5  30416  friendship  30427  grpodivdiv  30568  grpomuldivass  30569  ablodivdiv4  30582  ablonnncan1  30585  nvmdi  30676  dipassr  30874  archiabllem2c  33184  dvrcan5  33225  rloccring  33256  reofld  33351  eqgvscpbl  33357  qusvsval  33359  quslmod  33365  quslmhm  33366  dvdsruasso2  33393  prmidlc  33455  ssdifidl  33464  ssmxidl  33481  ply1degltlss  33596  r1plmhm  33609  drgextlsp  33622  ccfldsrarelvec  33695  constrconj  33749  constrfin  33750  constrelextdg2  33751  pstmfval  33856  tpr2rico  33872  qqhval2lem  33943  qqhvq  33949  issiga  34092  measdivcst  34204  measdivcstALTV  34205  carsggect  34299  signsply0  34544  tgoldbachgtd  34655  bnj149  34867  bnj1118  34976  bnj1128  34982  erdszelem9  35183  resconn  35230  cvmseu  35260  cvmlift2lem12  35298  ex-sategoelel  35405  elmrsubrn  35504  mclsind  35554  r1peuqusdeg1  35627  cgrid2  35984  segconeu  35992  btwncomim  35994  btwnswapid  35998  cgrxfr  36036  btwnxfr  36037  colineardim1  36042  brofs2  36058  brifs2  36059  idinside  36065  endofsegid  36066  btwnconn1lem7  36074  btwnconn1lem11  36078  btwnconn1  36082  segcon2  36086  seglemin  36094  segletr  36095  btwnsegle  36098  colinbtwnle  36099  broutsideof2  36103  broutsideof3  36107  outsidele  36113  fvray  36122  fvline  36125  linerflx1  36130  ellines  36133  ivthALT  36317  weiunpo  36447  poimirlem32  37638  ftc1anc  37687  sdclem1  37729  sstotbnd2  37760  zerdivemp1x  37933  isdrngo2  37944  iscringd  37984  lsmsat  38989  lfladdcl  39052  lflnegcl  39056  lflvscl  39058  lshpkrlem4  39094  lshpkrlem6  39096  ldualgrplem  39126  lduallmodlem  39133  latmassOLD  39210  latm12  39211  latm32  39212  latmrot  39213  latmmdiN  39215  latmmdir  39216  omlfh1N  39239  omlfh3N  39240  cvlexchb1  39311  cvlexch3  39313  cvlexch4N  39314  cvlatexchb1  39315  cvlsupr2  39324  hlatjass  39351  hlatj12  39352  hlatj32  39353  cvratlem  39403  cvrat  39404  atcvrj0  39410  cvrat2  39411  atltcvr  39417  atexchltN  39423  cvrat3  39424  cvrat4  39425  3dimlem3  39443  3dimlem3OLDN  39444  3at  39472  2atneat  39497  llncmp  39504  2at0mat0  39507  2atmat0  39508  lplnnle2at  39523  llncvrlpln  39540  lplncmp  39544  lplnexllnN  39546  2llnjaN  39548  4atlem11  39591  lplncvrlvol  39598  lvolcmp  39599  2atm2atN  39767  elpaddatriN  39785  paddasslem9  39810  paddass  39820  padd12N  39821  paddssw2  39826  paddss  39827  pmodlem2  39829  pmodN  39832  pmapjlln1  39837  atmod1i1  39839  atmod1i2  39841  pexmidlem2N  39953  pexmidlem6N  39957  pl42N  39965  lhpm0atN  40011  lautlt  40073  lautcvr  40074  lautj  40075  lautm  40076  ltrneq2  40130  cdlemc3  40175  cdlemc4  40176  cdlemd1  40180  cdleme1b  40208  cdleme1  40209  cdleme2  40210  cdleme3e  40214  cdlemefr27cl  40385  cdlemefs27cl  40395  cdleme42mN  40469  cdlemftr2  40548  trljco  40722  tgrpgrplem  40731  tendoplass  40765  tendodi1  40766  tendodi2  40767  cdlemk36  40895  erngdvlem3  40972  erngdvlem3-rN  40980  tendospdi1  41002  dvalveclem  41007  dialss  41028  dvhvaddass  41079  dvhopvsca  41084  dvhlveclem  41090  diblss  41152  diclss  41175  dihmeetlem12N  41300  dihmeetlem15N  41303  dihmeetlem16N  41304  dihmeetlem17N  41305  dihmeetlem18N  41306  dihmeetlem19N  41307  dvh4dimN  41429  lpolvN  41468  lclkr  41515  lclkrs  41521  lcfr  41567  aks6d1c1  42097  irrapxlem6  42814  jm2.26lem3  42989  dgrsub2  43123  mpaadgr  43142  mendring  43176  mendlmod  43177  mendassa  43178  nnoeomeqom  43301  omabs2  43321  relexpmulg  43699  iunrelexpmin2  43701  relexpxpmin  43706  neicvgel1  44108  fmuldfeq  45538  stoweidlem43  45998  stoweidlem52  46007  stoweidlem53  46008  stoweidlem56  46011  stoweidlem57  46012  issmfle  46700  issmfgt  46711  issmfge  46725  submodaddmod  47280  fmtnoprmfac1  47489  fmtnoprmfac2  47491  clnbgredg  47763  grlimgrtrilem1  47896  upgrwlkupwlk  47983  copissgrp  48011  cznrng  48104  funcringcsetcALTV2lem9  48141  funcringcsetclem9ALTV  48164  linccl  48259  lincext1  48299  lincext3  48301  lincresunit2  48323  line  48581  rrxline  48583  itsclc0yqsol  48613  topdlat  48792  catprs  48799  endmndlem  48803  idmon  48804  idepi  48805  thincmon  48833  thincepi  48834  grptcmon  48901  grptcepi  48902