Theorem simpr1 1213

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr11  1276  simpr21  1279  simpr31  1282  simp1r1  1288  simp2r1  1294  simp3r1  1300  3anandis  1500  fpr2g  7216  isopolem  7354  fr3nr  7780  sexp3  8158  suppfnss  8194  frrlem4  8295  frrlem8  8299  dif1en  9156  frfi  9255  intrnfi  9386  iinfi  9387  eqsup  9426  fisupcl  9440  cnfcomlem  9678  ttrclss  9699  ackbij1lem15  10235  fpwwe2lem4  10637  dedekindle  11392  ico0  13436  elioc2  13454  elico2  13455  elicc2  13456  iccsplit  13530  fseq1p1m1  13645  elfz0ubfz0  13679  hashtpg  14542  hash7g  14543  swrdsbslen  14726  ccatswrd  14730  wwlktovf1  15020  tanadd  16248  dvds2ln  16372  qredeq  16740  ressress  17332  mreexexlem4d  17728  mreexexd  17729  0catg  17769  2oppccomf  17806  issubc3  17931  fthmon  18011  fuccocl  18049  fucidcl  18050  invfuc  18059  initoeu2lem0  18095  initoeu2lem1  18096  curf2cl  18312  yonedalem4c  18358  yonedalem3  18361  pospo  18424  latjle12  18531  latjlej1  18534  latnlej2  18540  latlem12  18547  latmlem1  18550  latledi  18558  latmlej11  18559  latjass  18564  latj12  18565  latj32  18566  latj13  18567  latj31  18568  latjrot  18569  latjjdi  18572  latjjdir  18573  latdisdlem  18577  prdssgrpd  18820  prdsmndd  18859  imasmnd2  18863  mndissubm  18896  frmdmnd  18949  grpsubrcan  19118  grpsubadd  19125  grpsubsub  19126  grpaddsubass  19127  grpsubsub4  19130  grpnnncan2  19134  imasgrp2  19152  mulgnndir  19200  mulgnn0dir  19201  mulgdir  19203  mulgnnass  19206  mulgnn0ass  19207  mulgass  19208  mulgsubdir  19211  pwsmulg  19216  issubg2  19239  eqgval  19276  qusgrp  19288  kerf1ghm  19348  galcan  19405  gacan  19406  oppgmnd  19455  pmtrprfv  19554  pmtr3ncom  19576  psgnunilem3  19597  cmn32  19901  cmn12  19903  abladdsub  19913  ablsubaddsub  19915  mulgnn0di  19926  mulgdi  19927  mulgsubdi  19930  dprdss  20132  dprdz  20133  dprdf1o  20135  dprdsn  20139  dprd2da  20145  ablfac1b  20173  pgpfac1lem5  20182  prdsrngd  20285  imasrng  20286  srgbinomlem2  20340  srgbinom  20344  ringdilem  20362  prdsringd  20435  imasring  20445  opprrng  20460  mulgass3  20468  dvrass  20523  dvrdir  20527  subrgunit  20726  issubrg2  20728  abvdiv  20969  islss3  21117  prdslmodd  21127  islmhm2  21196  lspsolv  21304  islbs2  21315  islbs3  21316  lbsextlem4  21322  sralmod  21345  prmidlc  21510  ssdifidl  21522  ipdir  21826  ipdi  21827  ipsubdir  21829  ipsubdi  21830  ipass  21832  ipassr  21833  ipassr2  21834  ocvlss  21859  psrlmod  22146  psrring  22156  psrassa  22159  ply1ass23l  22423  mamudm  22589  matring  22637  matassa  22638  ofco2  22645  mdetunilem1  22806  mdetunilem9  22814  mdetuni0  22815  mdetmul  22817  gsummatr01lem3  22851  iinopn  23096  subbascn  23448  nrmsep2  23550  isnrm3  23553  regsep2  23570  dnsconst  23572  dfconn2  23613  1stcelcls  23655  nllyidm  23683  dislly  23691  upxp  23817  fbasne0  24024  filss  24047  infil  24057  fsubbas  24061  filssufilg  24105  tmdcn2  24283  psmettri  24505  isxmet2d  24521  xmettri  24545  xmetres2  24555  bldisj  24592  blss2ps  24597  blss2  24598  xmstri2  24660  mstri2  24661  xmstri  24662  mstri  24663  xmstri3  24664  mstri3  24665  msrtri  24666  comet  24707  stdbdbl  24711  met2ndci  24716  ngprcan  24804  ngplcan  24805  ngpsubcan  24808  nmtri2  24821  nrgdsdi  24859  nrgdsdir  24860  nlmdsdi  24875  nlmdsdir  24876  blcvx  24992  icccmplem2  25018  pi1grplem  25245  pi1cof  25255  clmpm1dir  25299  cvsdiv  25328  cvsdivcl  25329  cphdivcl  25378  cphsubdir  25404  cphsubdi  25405  cphassr  25408  bcthlem5  25524  rrxcph  25588  volfiniun  25743  volcn  25802  itg1val2  25880  dvconst  26113  dvlip  26189  dvfsumlem4  26225  ftc1a  26233  ulmval  26580  ulmdvlem3  26602  ang180  27016  cvxcl  27186  scvxcvx  27187  sgmmul  27402  logexprlim  27426  dchrabl  27455  nosupbnd1  27915  noinfbnd1lem5  27928  noinfbnd1  27930  sltsss1  27995  motgrp  28849  iscgra1  29158  cgrane1  29160  cgrane2  29161  cgrahl1  29164  cgrahl2  29165  cgracgr  29166  cgratr  29171  cgrabtwn  29174  dfcgra2  29178  sacgr  29179  f1otrge  29258  colinearalglem1  29293  colinearalg  29297  axcgrtr  29302  axlowdimlem16  29344  axeuclidlem  29349  axcontlem7  29357  eengtrkg  29373  eengtrkge  29374  nbfusgrlevtxm2  29765  lfgriswlk  30073  upgrwlkdvde  30123  wwlknbp1  30230  usgrwwlks2on  30344  erclwwlktr  30410  erclwwlkntr  30459  frgr2wwlkeqm  30719  numclwwlk1lem2f  30743  numclwwlk5  30776  friendship  30787  grpodivdiv  30929  grpomuldivass  30930  ablodivdiv4  30943  ablonnncan1  30946  nvmdi  31037  dipassr  31235  archiabllem2c  33546  dvrcan5  33586  rloccring  33622  reofld  33694  eqgvscpbl  33701  qusvsval  33703  quslmod  33709  quslmhm  33710  dvdsruasso2  33730  ssmxidl  33788  ply1degltlss  33917  r1plmhm  33930  drgextlsp  34015  ccfldsrarelvec  34092  constrconj  34166  constrfin  34167  constrelextdg2  34168  pstmfval  34317  tpr2rico  34333  qqhval2lem  34402  qqhvq  34408  issiga  34533  measdivcst  34646  measdivcstALTV  34647  carsggect  34740  signsply0  34970  tgoldbachgtd  35081  bnj149  35295  bnj1118  35404  bnj1128  35410  erdszelem9  35712  resconn  35759  cvmseu  35789  cvmlift2lem12  35827  ex-sategoelel  35934  elmrsubrn  36033  mclsind  36083  r1peuqusdeg1  36156  cgrid2  36516  segconeu  36524  btwncomim  36526  btwnswapid  36530  cgrxfr  36568  btwnxfr  36569  colineardim1  36574  brofs2  36590  brifs2  36591  idinside  36597  endofsegid  36598  btwnconn1lem7  36606  btwnconn1lem11  36610  btwnconn1  36614  segcon2  36618  seglemin  36626  segletr  36627  btwnsegle  36630  colinbtwnle  36631  broutsideof2  36635  broutsideof3  36639  outsidele  36645  fvray  36654  fvline  36657  linerflx1  36662  ellines  36665  ivthALT  36887  weiunpo  37017  poimirlem32  38344  ftc1anc  38393  sdclem1  38435  sstotbnd2  38466  zerdivemp1x  38639  isdrngo2  38650  iscringd  38690  lsmsat  39823  lfladdcl  39886  lflnegcl  39890  lflvscl  39892  lshpkrlem4  39928  lshpkrlem6  39930  ldualgrplem  39960  lduallmodlem  39967  latmassOLD  40044  latm12  40045  latm32  40046  latmrot  40047  latmmdiN  40049  latmmdir  40050  omlfh1N  40073  omlfh3N  40074  cvlexchb1  40145  cvlexch3  40147  cvlexch4N  40148  cvlatexchb1  40149  cvlsupr2  40158  hlatjass  40185  hlatj12  40186  hlatj32  40187  cvratlem  40236  cvrat  40237  atcvrj0  40243  cvrat2  40244  atltcvr  40250  atexchltN  40256  cvrat3  40257  cvrat4  40258  3dimlem3  40276  3dimlem3OLDN  40277  3at  40305  2atneat  40330  llncmp  40337  2at0mat0  40340  2atmat0  40341  lplnnle2at  40356  llncvrlpln  40373  lplncmp  40377  lplnexllnN  40379  2llnjaN  40381  4atlem11  40424  lplncvrlvol  40431  lvolcmp  40432  2atm2atN  40600  elpaddatriN  40618  paddasslem9  40643  paddass  40653  padd12N  40654  paddssw2  40659  paddss  40660  pmodlem2  40662  pmodN  40665  pmapjlln1  40670  atmod1i1  40672  atmod1i2  40674  pexmidlem2N  40786  pexmidlem6N  40790  pl42N  40798  lhpm0atN  40844  lautlt  40906  lautcvr  40907  lautj  40908  lautm  40909  ltrneq2  40963  cdlemc3  41008  cdlemc4  41009  cdlemd1  41013  cdleme1b  41041  cdleme1  41042  cdleme2  41043  cdleme3e  41047  cdlemefr27cl  41218  cdlemefs27cl  41228  cdleme42mN  41302  cdlemftr2  41381  trljco  41555  tgrpgrplem  41564  tendoplass  41598  tendodi1  41599  tendodi2  41600  cdlemk36  41728  erngdvlem3  41805  erngdvlem3-rN  41813  tendospdi1  41835  dvalveclem  41840  dialss  41861  dvhvaddass  41912  dvhopvsca  41917  dvhlveclem  41923  diblss  41985  diclss  42008  dihmeetlem12N  42133  dihmeetlem15N  42136  dihmeetlem16N  42137  dihmeetlem17N  42138  dihmeetlem18N  42139  dihmeetlem19N  42140  dvh4dimN  42262  lpolvN  42301  lclkr  42348  lclkrs  42354  lcfr  42400  aks6d1c1  42924  irrapxlem6  43595  jm2.26lem3  43769  dgrsub2  43903  mpaadgr  43922  mendring  43956  mendlmod  43957  mendassa  43958  nnoeomeqom  44080  omabs2  44100  relexpmulg  44477  iunrelexpmin2  44479  relexpxpmin  44484  neicvgel1  44886  fmuldfeq  46340  stoweidlem43  46798  stoweidlem52  46807  stoweidlem53  46808  stoweidlem56  46811  stoweidlem57  46812  issmfle  47500  issmfgt  47511  issmfge  47525  submodaddmod  48125  fmtnoprmfac1  48358  fmtnoprmfac2  48360  clnbgredg  48646  cycl3grtrilem  48752  grlimprclnbgr  48802  grlimprclnbgredg  48803  upgrwlkupwlk  48946  copissgrp  48974  cznrng  49067  funcringcsetcALTV2lem9  49104  funcringcsetclem9ALTV  49127  idomcanl  49153  linccl  49235  lincext1  49275  lincext3  49277  lincresunit2  49299  line  49553  rrxline  49555  itsclc0yqsol  49585  resipos  49794  topdlat  49823  catprs  49830  endmndlem  49834  idmon  49839  idepi  49840  thincmon  50252  thincepi  50253  grptcmon  50412  grptcepi  50413