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  7185  isopolem  7320  fr3nr  7748  sexp3  8132  suppfnss  8168  frrlem4  8268  frrlem8  8272  dif1en  9124  frfi  9232  intrnfi  9367  iinfi  9368  eqsup  9407  fisupcl  9421  cnfcomlem  9652  ttrclss  9673  ackbij1lem15  10186  fpwwe2lem4  10587  dedekindle  11338  ico0  13352  elioc2  13370  elico2  13371  elicc2  13372  iccsplit  13446  fseq1p1m1  13559  elfz0ubfz0  13593  hashtpg  14450  hash7g  14451  swrdsbslen  14629  ccatswrd  14633  wwlktovf1  14923  tanadd  16135  dvds2ln  16259  qredeq  16627  ressress  17217  mreexexlem4d  17608  mreexexd  17609  0catg  17649  2oppccomf  17686  issubc3  17811  fthmon  17891  fuccocl  17929  fucidcl  17930  invfuc  17939  initoeu2lem0  17975  initoeu2lem1  17976  curf2cl  18192  yonedalem4c  18238  yonedalem3  18241  pospo  18304  latjle12  18409  latjlej1  18412  latnlej2  18418  latlem12  18425  latmlem1  18428  latledi  18436  latmlej11  18437  latjass  18442  latj12  18443  latj32  18444  latj13  18445  latj31  18446  latjrot  18447  latjjdi  18450  latjjdir  18451  latdisdlem  18455  prdssgrpd  18660  prdsmndd  18697  imasmnd2  18701  mndissubm  18734  frmdmnd  18786  grpsubrcan  18953  grpsubadd  18960  grpsubsub  18961  grpaddsubass  18962  grpsubsub4  18965  grpnnncan2  18969  imasgrp2  18987  mulgnndir  19035  mulgnn0dir  19036  mulgdir  19038  mulgnnass  19041  mulgnn0ass  19042  mulgass  19043  mulgsubdir  19046  pwsmulg  19051  issubg2  19073  eqgval  19109  qusgrp  19118  kerf1ghm  19179  galcan  19236  gacan  19237  oppgmnd  19286  pmtrprfv  19383  pmtr3ncom  19405  psgnunilem3  19426  cmn32  19730  cmn12  19732  abladdsub  19742  ablsubaddsub  19744  mulgnn0di  19755  mulgdi  19756  mulgsubdi  19759  dprdss  19961  dprdz  19962  dprdf1o  19964  dprdsn  19968  dprd2da  19974  ablfac1b  20002  pgpfac1lem5  20011  prdsrngd  20085  imasrng  20086  srgbinomlem2  20136  srgbinom  20140  ringdilem  20158  prdsringd  20230  imasring  20239  opprrng  20254  mulgass3  20262  dvrass  20317  dvrdir  20321  subrgunit  20499  issubrg2  20501  abvdiv  20738  islss3  20865  prdslmodd  20875  islmhm2  20945  lspsolv  21053  islbs2  21064  islbs3  21065  lbsextlem4  21071  sralmod  21094  ipdir  21548  ipdi  21549  ipsubdir  21551  ipsubdi  21552  ipass  21554  ipassr  21555  ipassr2  21556  ocvlss  21581  sraassaOLD  21779  psrgrpOLD  21866  psrlmod  21869  psrring  21879  psrassa  21882  ply1ass23l  22111  mamudm  22282  matring  22330  matassa  22331  ofco2  22338  mdetunilem1  22499  mdetunilem9  22507  mdetuni0  22508  mdetmul  22510  gsummatr01lem3  22544  iinopn  22789  subbascn  23141  nrmsep2  23243  isnrm3  23246  regsep2  23263  dnsconst  23265  dfconn2  23306  1stcelcls  23348  nllyidm  23376  dislly  23384  upxp  23510  fbasne0  23717  filss  23740  infil  23750  fsubbas  23754  filssufilg  23798  tmdcn2  23976  psmettri  24199  isxmet2d  24215  xmettri  24239  xmetres2  24249  bldisj  24286  blss2ps  24291  blss2  24292  xmstri2  24354  mstri2  24355  xmstri  24356  mstri  24357  xmstri3  24358  mstri3  24359  msrtri  24360  comet  24401  stdbdbl  24405  met2ndci  24410  ngprcan  24498  ngplcan  24499  ngpsubcan  24502  nmtri2  24515  nrgdsdi  24553  nrgdsdir  24554  nlmdsdi  24569  nlmdsdir  24570  blcvx  24686  icccmplem2  24712  pi1grplem  24949  pi1cof  24959  clmpm1dir  25003  cvsdiv  25032  cvsdivcl  25033  cphdivcl  25082  cphsubdir  25108  cphsubdi  25109  cphassr  25112  bcthlem5  25228  rrxcph  25292  volfiniun  25448  volcn  25507  itg1val2  25585  dvconst  25818  dvlip  25898  dvfsumlem4  25936  ftc1a  25944  ulmval  26289  ulmdvlem3  26311  ang180  26724  cvxcl  26895  scvxcvx  26896  sgmmul  27112  logexprlim  27136  dchrabl  27165  nosupbnd1  27626  noinfbnd1lem5  27639  noinfbnd1  27641  ssltss1  27700  motgrp  28470  iscgra1  28737  cgrane1  28739  cgrane2  28740  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgratr  28750  cgrabtwn  28753  dfcgra2  28757  sacgr  28758  f1otrge  28799  colinearalglem1  28833  colinearalg  28837  axcgrtr  28842  axlowdimlem16  28884  axeuclidlem  28889  axcontlem7  28897  eengtrkg  28913  eengtrkge  28914  nbfusgrlevtxm2  29305  lfgriswlk  29616  upgrwlkdvde  29667  wwlknbp1  29774  erclwwlktr  29951  erclwwlkntr  30000  frgr2wwlkeqm  30260  numclwwlk1lem2f  30284  numclwwlk5  30317  friendship  30328  grpodivdiv  30469  grpomuldivass  30470  ablodivdiv4  30483  ablonnncan1  30486  nvmdi  30577  dipassr  30775  archiabllem2c  33149  dvrcan5  33187  rloccring  33221  reofld  33315  eqgvscpbl  33321  qusvsval  33323  quslmod  33329  quslmhm  33330  dvdsruasso2  33357  prmidlc  33419  ssdifidl  33428  ssmxidl  33445  ply1degltlss  33562  r1plmhm  33575  drgextlsp  33589  ccfldsrarelvec  33666  constrconj  33735  constrfin  33736  constrelextdg2  33737  pstmfval  33886  tpr2rico  33902  qqhval2lem  33971  qqhvq  33977  issiga  34102  measdivcst  34214  measdivcstALTV  34215  carsggect  34309  signsply0  34542  tgoldbachgtd  34653  bnj149  34865  bnj1118  34974  bnj1128  34980  erdszelem9  35186  resconn  35233  cvmseu  35263  cvmlift2lem12  35301  ex-sategoelel  35408  elmrsubrn  35507  mclsind  35557  r1peuqusdeg1  35630  cgrid2  35991  segconeu  35999  btwncomim  36001  btwnswapid  36005  cgrxfr  36043  btwnxfr  36044  colineardim1  36049  brofs2  36065  brifs2  36066  idinside  36072  endofsegid  36073  btwnconn1lem7  36081  btwnconn1lem11  36085  btwnconn1  36089  segcon2  36093  seglemin  36101  segletr  36102  btwnsegle  36105  colinbtwnle  36106  broutsideof2  36110  broutsideof3  36114  outsidele  36120  fvray  36129  fvline  36132  linerflx1  36137  ellines  36140  ivthALT  36323  weiunpo  36453  poimirlem32  37646  ftc1anc  37695  sdclem1  37737  sstotbnd2  37768  zerdivemp1x  37941  isdrngo2  37952  iscringd  37992  lsmsat  39001  lfladdcl  39064  lflnegcl  39068  lflvscl  39070  lshpkrlem4  39106  lshpkrlem6  39108  ldualgrplem  39138  lduallmodlem  39145  latmassOLD  39222  latm12  39223  latm32  39224  latmrot  39225  latmmdiN  39227  latmmdir  39228  omlfh1N  39251  omlfh3N  39252  cvlexchb1  39323  cvlexch3  39325  cvlexch4N  39326  cvlatexchb1  39327  cvlsupr2  39336  hlatjass  39363  hlatj12  39364  hlatj32  39365  cvratlem  39415  cvrat  39416  atcvrj0  39422  cvrat2  39423  atltcvr  39429  atexchltN  39435  cvrat3  39436  cvrat4  39437  3dimlem3  39455  3dimlem3OLDN  39456  3at  39484  2atneat  39509  llncmp  39516  2at0mat0  39519  2atmat0  39520  lplnnle2at  39535  llncvrlpln  39552  lplncmp  39556  lplnexllnN  39558  2llnjaN  39560  4atlem11  39603  lplncvrlvol  39610  lvolcmp  39611  2atm2atN  39779  elpaddatriN  39797  paddasslem9  39822  paddass  39832  padd12N  39833  paddssw2  39838  paddss  39839  pmodlem2  39841  pmodN  39844  pmapjlln1  39849  atmod1i1  39851  atmod1i2  39853  pexmidlem2N  39965  pexmidlem6N  39969  pl42N  39977  lhpm0atN  40023  lautlt  40085  lautcvr  40086  lautj  40087  lautm  40088  ltrneq2  40142  cdlemc3  40187  cdlemc4  40188  cdlemd1  40192  cdleme1b  40220  cdleme1  40221  cdleme2  40222  cdleme3e  40226  cdlemefr27cl  40397  cdlemefs27cl  40407  cdleme42mN  40481  cdlemftr2  40560  trljco  40734  tgrpgrplem  40743  tendoplass  40777  tendodi1  40778  tendodi2  40779  cdlemk36  40907  erngdvlem3  40984  erngdvlem3-rN  40992  tendospdi1  41014  dvalveclem  41019  dialss  41040  dvhvaddass  41091  dvhopvsca  41096  dvhlveclem  41102  diblss  41164  diclss  41187  dihmeetlem12N  41312  dihmeetlem15N  41315  dihmeetlem16N  41316  dihmeetlem17N  41317  dihmeetlem18N  41318  dihmeetlem19N  41319  dvh4dimN  41441  lpolvN  41480  lclkr  41527  lclkrs  41533  lcfr  41579  aks6d1c1  42104  irrapxlem6  42815  jm2.26lem3  42990  dgrsub2  43124  mpaadgr  43143  mendring  43177  mendlmod  43178  mendassa  43179  nnoeomeqom  43301  omabs2  43321  relexpmulg  43699  iunrelexpmin2  43701  relexpxpmin  43706  neicvgel1  44108  fmuldfeq  45581  stoweidlem43  46041  stoweidlem52  46050  stoweidlem53  46051  stoweidlem56  46054  stoweidlem57  46055  issmfle  46743  issmfgt  46754  issmfge  46768  submodaddmod  47342  fmtnoprmfac1  47566  fmtnoprmfac2  47568  clnbgredg  47840  cycl3grtrilem  47945  grlimgrtrilem1  47993  upgrwlkupwlk  48128  copissgrp  48156  cznrng  48249  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  linccl  48403  lincext1  48443  lincext3  48445  lincresunit2  48467  line  48721  rrxline  48723  itsclc0yqsol  48753  resipos  48963  topdlat  48992  catprs  49000  endmndlem  49004  idmon  49009  idepi  49010  thincmon  49422  thincepi  49423  grptcmon  49582  grptcepi  49583