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 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  1258  simpr21  1261  simpr31  1264  simp1r1  1270  simp2r1  1276  simp3r1  1282  3anandis  1473  fpr2g  7231  isopolem  7365  fr3nr  7792  sexp3  8178  suppfnss  8214  frrlem4  8314  frrlem8  8318  dif1en  9200  frfi  9321  intrnfi  9456  iinfi  9457  eqsup  9496  fisupcl  9509  cnfcomlem  9739  ttrclss  9760  ackbij1lem15  10273  fpwwe2lem4  10674  dedekindle  11425  ico0  13433  elioc2  13450  elico2  13451  elicc2  13452  iccsplit  13525  fseq1p1m1  13638  elfz0ubfz0  13672  hashtpg  14524  hash7g  14525  swrdsbslen  14702  ccatswrd  14706  wwlktovf1  14996  tanadd  16203  dvds2ln  16326  qredeq  16694  ressress  17293  mreexexlem4d  17690  mreexexd  17691  0catg  17731  2oppccomf  17768  issubc3  17894  fthmon  17974  fuccocl  18012  fucidcl  18013  invfuc  18022  initoeu2lem0  18058  initoeu2lem1  18059  curf2cl  18276  yonedalem4c  18322  yonedalem3  18325  pospo  18390  latjle12  18495  latjlej1  18498  latnlej2  18504  latlem12  18511  latmlem1  18514  latledi  18522  latmlej11  18523  latjass  18528  latj12  18529  latj32  18530  latj13  18531  latj31  18532  latjrot  18533  latjjdi  18536  latjjdir  18537  latdisdlem  18541  prdssgrpd  18746  prdsmndd  18783  imasmnd2  18787  mndissubm  18820  frmdmnd  18872  grpsubrcan  19039  grpsubadd  19046  grpsubsub  19047  grpaddsubass  19048  grpsubsub4  19051  grpnnncan2  19055  imasgrp2  19073  mulgnndir  19121  mulgnn0dir  19122  mulgdir  19124  mulgnnass  19127  mulgnn0ass  19128  mulgass  19129  mulgsubdir  19132  pwsmulg  19137  issubg2  19159  eqgval  19195  qusgrp  19204  kerf1ghm  19265  galcan  19322  gacan  19323  oppgmnd  19373  pmtrprfv  19471  pmtr3ncom  19493  psgnunilem3  19514  cmn32  19818  cmn12  19820  abladdsub  19830  ablsubaddsub  19832  mulgnn0di  19843  mulgdi  19844  mulgsubdi  19847  dprdss  20049  dprdz  20050  dprdf1o  20052  dprdsn  20056  dprd2da  20062  ablfac1b  20090  pgpfac1lem5  20099  prdsrngd  20173  imasrng  20174  srgbinomlem2  20224  srgbinom  20228  ringdilem  20246  prdsringd  20318  imasring  20327  opprrng  20345  mulgass3  20353  dvrass  20408  dvrdir  20412  subrgunit  20590  issubrg2  20592  abvdiv  20830  islss3  20957  prdslmodd  20967  islmhm2  21037  lspsolv  21145  islbs2  21156  islbs3  21157  lbsextlem4  21163  sralmod  21194  ipdir  21657  ipdi  21658  ipsubdir  21660  ipsubdi  21661  ipass  21663  ipassr  21664  ipassr2  21665  ocvlss  21690  sraassaOLD  21890  psrgrpOLD  21977  psrlmod  21980  psrring  21990  psrassa  21993  ply1ass23l  22228  mamudm  22399  matring  22449  matassa  22450  ofco2  22457  mdetunilem1  22618  mdetunilem9  22626  mdetuni0  22627  mdetmul  22629  gsummatr01lem3  22663  iinopn  22908  subbascn  23262  nrmsep2  23364  isnrm3  23367  regsep2  23384  dnsconst  23386  dfconn2  23427  1stcelcls  23469  nllyidm  23497  dislly  23505  upxp  23631  fbasne0  23838  filss  23861  infil  23871  fsubbas  23875  filssufilg  23919  tmdcn2  24097  psmettri  24321  isxmet2d  24337  xmettri  24361  xmetres2  24371  bldisj  24408  blss2ps  24413  blss2  24414  xmstri2  24476  mstri2  24477  xmstri  24478  mstri  24479  xmstri3  24480  mstri3  24481  msrtri  24482  comet  24526  stdbdbl  24530  met2ndci  24535  ngprcan  24623  ngplcan  24624  ngpsubcan  24627  nmtri2  24640  nrgdsdi  24686  nrgdsdir  24687  nlmdsdi  24702  nlmdsdir  24703  blcvx  24819  icccmplem2  24845  pi1grplem  25082  pi1cof  25092  clmpm1dir  25136  cvsdiv  25165  cvsdivcl  25166  cphdivcl  25216  cphsubdir  25242  cphsubdi  25243  cphassr  25246  bcthlem5  25362  rrxcph  25426  volfiniun  25582  volcn  25641  itg1val2  25719  dvconst  25952  dvlip  26032  dvfsumlem4  26070  ftc1a  26078  ulmval  26423  ulmdvlem3  26445  ang180  26857  cvxcl  27028  scvxcvx  27029  sgmmul  27245  logexprlim  27269  dchrabl  27298  nosupbnd1  27759  noinfbnd1lem5  27772  noinfbnd1  27774  ssltss1  27833  motgrp  28551  iscgra1  28818  cgrane1  28820  cgrane2  28821  cgrahl1  28824  cgrahl2  28825  cgracgr  28826  cgratr  28831  cgrabtwn  28834  dfcgra2  28838  sacgr  28839  f1otrge  28880  colinearalglem1  28921  colinearalg  28925  axcgrtr  28930  axlowdimlem16  28972  axeuclidlem  28977  axcontlem7  28985  eengtrkg  29001  eengtrkge  29002  nbfusgrlevtxm2  29395  lfgriswlk  29706  upgrwlkdvde  29757  wwlknbp1  29864  erclwwlktr  30041  erclwwlkntr  30090  frgr2wwlkeqm  30350  numclwwlk1lem2f  30374  numclwwlk5  30407  friendship  30418  grpodivdiv  30559  grpomuldivass  30560  ablodivdiv4  30573  ablonnncan1  30576  nvmdi  30667  dipassr  30865  archiabllem2c  33202  dvrcan5  33240  rloccring  33274  reofld  33372  eqgvscpbl  33378  qusvsval  33380  quslmod  33386  quslmhm  33387  dvdsruasso2  33414  prmidlc  33476  ssdifidl  33485  ssmxidl  33502  ply1degltlss  33617  r1plmhm  33630  drgextlsp  33644  ccfldsrarelvec  33721  constrconj  33786  constrfin  33787  constrelextdg2  33788  pstmfval  33895  tpr2rico  33911  qqhval2lem  33982  qqhvq  33988  issiga  34113  measdivcst  34225  measdivcstALTV  34226  carsggect  34320  signsply0  34566  tgoldbachgtd  34677  bnj149  34889  bnj1118  34998  bnj1128  35004  erdszelem9  35204  resconn  35251  cvmseu  35281  cvmlift2lem12  35319  ex-sategoelel  35426  elmrsubrn  35525  mclsind  35575  r1peuqusdeg1  35648  cgrid2  36004  segconeu  36012  btwncomim  36014  btwnswapid  36018  cgrxfr  36056  btwnxfr  36057  colineardim1  36062  brofs2  36078  brifs2  36079  idinside  36085  endofsegid  36086  btwnconn1lem7  36094  btwnconn1lem11  36098  btwnconn1  36102  segcon2  36106  seglemin  36114  segletr  36115  btwnsegle  36118  colinbtwnle  36119  broutsideof2  36123  broutsideof3  36127  outsidele  36133  fvray  36142  fvline  36145  linerflx1  36150  ellines  36153  ivthALT  36336  weiunpo  36466  poimirlem32  37659  ftc1anc  37708  sdclem1  37750  sstotbnd2  37781  zerdivemp1x  37954  isdrngo2  37965  iscringd  38005  lsmsat  39009  lfladdcl  39072  lflnegcl  39076  lflvscl  39078  lshpkrlem4  39114  lshpkrlem6  39116  ldualgrplem  39146  lduallmodlem  39153  latmassOLD  39230  latm12  39231  latm32  39232  latmrot  39233  latmmdiN  39235  latmmdir  39236  omlfh1N  39259  omlfh3N  39260  cvlexchb1  39331  cvlexch3  39333  cvlexch4N  39334  cvlatexchb1  39335  cvlsupr2  39344  hlatjass  39371  hlatj12  39372  hlatj32  39373  cvratlem  39423  cvrat  39424  atcvrj0  39430  cvrat2  39431  atltcvr  39437  atexchltN  39443  cvrat3  39444  cvrat4  39445  3dimlem3  39463  3dimlem3OLDN  39464  3at  39492  2atneat  39517  llncmp  39524  2at0mat0  39527  2atmat0  39528  lplnnle2at  39543  llncvrlpln  39560  lplncmp  39564  lplnexllnN  39566  2llnjaN  39568  4atlem11  39611  lplncvrlvol  39618  lvolcmp  39619  2atm2atN  39787  elpaddatriN  39805  paddasslem9  39830  paddass  39840  padd12N  39841  paddssw2  39846  paddss  39847  pmodlem2  39849  pmodN  39852  pmapjlln1  39857  atmod1i1  39859  atmod1i2  39861  pexmidlem2N  39973  pexmidlem6N  39977  pl42N  39985  lhpm0atN  40031  lautlt  40093  lautcvr  40094  lautj  40095  lautm  40096  ltrneq2  40150  cdlemc3  40195  cdlemc4  40196  cdlemd1  40200  cdleme1b  40228  cdleme1  40229  cdleme2  40230  cdleme3e  40234  cdlemefr27cl  40405  cdlemefs27cl  40415  cdleme42mN  40489  cdlemftr2  40568  trljco  40742  tgrpgrplem  40751  tendoplass  40785  tendodi1  40786  tendodi2  40787  cdlemk36  40915  erngdvlem3  40992  erngdvlem3-rN  41000  tendospdi1  41022  dvalveclem  41027  dialss  41048  dvhvaddass  41099  dvhopvsca  41104  dvhlveclem  41110  diblss  41172  diclss  41195  dihmeetlem12N  41320  dihmeetlem15N  41323  dihmeetlem16N  41324  dihmeetlem17N  41325  dihmeetlem18N  41326  dihmeetlem19N  41327  dvh4dimN  41449  lpolvN  41488  lclkr  41535  lclkrs  41541  lcfr  41587  aks6d1c1  42117  irrapxlem6  42838  jm2.26lem3  43013  dgrsub2  43147  mpaadgr  43166  mendring  43200  mendlmod  43201  mendassa  43202  nnoeomeqom  43325  omabs2  43345  relexpmulg  43723  iunrelexpmin2  43725  relexpxpmin  43730  neicvgel1  44132  fmuldfeq  45598  stoweidlem43  46058  stoweidlem52  46067  stoweidlem53  46068  stoweidlem56  46071  stoweidlem57  46072  issmfle  46760  issmfgt  46771  issmfge  46785  submodaddmod  47343  fmtnoprmfac1  47552  fmtnoprmfac2  47554  clnbgredg  47826  cycl3grtrilem  47913  grlimgrtrilem1  47961  upgrwlkupwlk  48056  copissgrp  48084  cznrng  48177  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237  linccl  48331  lincext1  48371  lincext3  48373  lincresunit2  48395  line  48653  rrxline  48655  itsclc0yqsol  48685  topdlat  48893  catprs  48900  endmndlem  48904  idmon  48908  idepi  48909  thincmon  49082  thincepi  49083  grptcmon  49190  grptcepi  49191