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  7202  isopolem  7337  fr3nr  7764  sexp3  8150  suppfnss  8186  frrlem4  8286  frrlem8  8290  dif1en  9172  frfi  9291  intrnfi  9426  iinfi  9427  eqsup  9466  fisupcl  9480  cnfcomlem  9711  ttrclss  9732  ackbij1lem15  10245  fpwwe2lem4  10646  dedekindle  11397  ico0  13406  elioc2  13424  elico2  13425  elicc2  13426  iccsplit  13500  fseq1p1m1  13613  elfz0ubfz0  13647  hashtpg  14501  hash7g  14502  swrdsbslen  14680  ccatswrd  14684  wwlktovf1  14974  tanadd  16183  dvds2ln  16306  qredeq  16674  ressress  17266  mreexexlem4d  17657  mreexexd  17658  0catg  17698  2oppccomf  17735  issubc3  17860  fthmon  17940  fuccocl  17978  fucidcl  17979  invfuc  17988  initoeu2lem0  18024  initoeu2lem1  18025  curf2cl  18241  yonedalem4c  18287  yonedalem3  18290  pospo  18353  latjle12  18458  latjlej1  18461  latnlej2  18467  latlem12  18474  latmlem1  18477  latledi  18485  latmlej11  18486  latjass  18491  latj12  18492  latj32  18493  latj13  18494  latj31  18495  latjrot  18496  latjjdi  18499  latjjdir  18500  latdisdlem  18504  prdssgrpd  18709  prdsmndd  18746  imasmnd2  18750  mndissubm  18783  frmdmnd  18835  grpsubrcan  19002  grpsubadd  19009  grpsubsub  19010  grpaddsubass  19011  grpsubsub4  19014  grpnnncan2  19018  imasgrp2  19036  mulgnndir  19084  mulgnn0dir  19085  mulgdir  19087  mulgnnass  19090  mulgnn0ass  19091  mulgass  19092  mulgsubdir  19095  pwsmulg  19100  issubg2  19122  eqgval  19158  qusgrp  19167  kerf1ghm  19228  galcan  19285  gacan  19286  oppgmnd  19335  pmtrprfv  19432  pmtr3ncom  19454  psgnunilem3  19475  cmn32  19779  cmn12  19781  abladdsub  19791  ablsubaddsub  19793  mulgnn0di  19804  mulgdi  19805  mulgsubdi  19808  dprdss  20010  dprdz  20011  dprdf1o  20013  dprdsn  20017  dprd2da  20023  ablfac1b  20051  pgpfac1lem5  20060  prdsrngd  20134  imasrng  20135  srgbinomlem2  20185  srgbinom  20189  ringdilem  20207  prdsringd  20279  imasring  20288  opprrng  20303  mulgass3  20311  dvrass  20366  dvrdir  20370  subrgunit  20548  issubrg2  20550  abvdiv  20787  islss3  20914  prdslmodd  20924  islmhm2  20994  lspsolv  21102  islbs2  21113  islbs3  21114  lbsextlem4  21120  sralmod  21143  ipdir  21597  ipdi  21598  ipsubdir  21600  ipsubdi  21601  ipass  21603  ipassr  21604  ipassr2  21605  ocvlss  21630  sraassaOLD  21828  psrgrpOLD  21915  psrlmod  21918  psrring  21928  psrassa  21931  ply1ass23l  22160  mamudm  22331  matring  22379  matassa  22380  ofco2  22387  mdetunilem1  22548  mdetunilem9  22556  mdetuni0  22557  mdetmul  22559  gsummatr01lem3  22593  iinopn  22838  subbascn  23190  nrmsep2  23292  isnrm3  23295  regsep2  23312  dnsconst  23314  dfconn2  23355  1stcelcls  23397  nllyidm  23425  dislly  23433  upxp  23559  fbasne0  23766  filss  23789  infil  23799  fsubbas  23803  filssufilg  23847  tmdcn2  24025  psmettri  24248  isxmet2d  24264  xmettri  24288  xmetres2  24298  bldisj  24335  blss2ps  24340  blss2  24341  xmstri2  24403  mstri2  24404  xmstri  24405  mstri  24406  xmstri3  24407  mstri3  24408  msrtri  24409  comet  24450  stdbdbl  24454  met2ndci  24459  ngprcan  24547  ngplcan  24548  ngpsubcan  24551  nmtri2  24564  nrgdsdi  24602  nrgdsdir  24603  nlmdsdi  24618  nlmdsdir  24619  blcvx  24735  icccmplem2  24761  pi1grplem  24998  pi1cof  25008  clmpm1dir  25052  cvsdiv  25081  cvsdivcl  25082  cphdivcl  25132  cphsubdir  25158  cphsubdi  25159  cphassr  25162  bcthlem5  25278  rrxcph  25342  volfiniun  25498  volcn  25557  itg1val2  25635  dvconst  25868  dvlip  25948  dvfsumlem4  25986  ftc1a  25994  ulmval  26339  ulmdvlem3  26361  ang180  26774  cvxcl  26945  scvxcvx  26946  sgmmul  27162  logexprlim  27186  dchrabl  27215  nosupbnd1  27676  noinfbnd1lem5  27689  noinfbnd1  27691  ssltss1  27750  motgrp  28468  iscgra1  28735  cgrane1  28737  cgrane2  28738  cgrahl1  28741  cgrahl2  28742  cgracgr  28743  cgratr  28748  cgrabtwn  28751  dfcgra2  28755  sacgr  28756  f1otrge  28797  colinearalglem1  28831  colinearalg  28835  axcgrtr  28840  axlowdimlem16  28882  axeuclidlem  28887  axcontlem7  28895  eengtrkg  28911  eengtrkge  28912  nbfusgrlevtxm2  29303  lfgriswlk  29614  upgrwlkdvde  29665  wwlknbp1  29772  erclwwlktr  29949  erclwwlkntr  29998  frgr2wwlkeqm  30258  numclwwlk1lem2f  30282  numclwwlk5  30315  friendship  30326  grpodivdiv  30467  grpomuldivass  30468  ablodivdiv4  30481  ablonnncan1  30484  nvmdi  30575  dipassr  30773  archiabllem2c  33139  dvrcan5  33177  rloccring  33211  reofld  33305  eqgvscpbl  33311  qusvsval  33313  quslmod  33319  quslmhm  33320  dvdsruasso2  33347  prmidlc  33409  ssdifidl  33418  ssmxidl  33435  ply1degltlss  33552  r1plmhm  33565  drgextlsp  33579  ccfldsrarelvec  33658  constrconj  33725  constrfin  33726  constrelextdg2  33727  pstmfval  33873  tpr2rico  33889  qqhval2lem  33958  qqhvq  33964  issiga  34089  measdivcst  34201  measdivcstALTV  34202  carsggect  34296  signsply0  34529  tgoldbachgtd  34640  bnj149  34852  bnj1118  34961  bnj1128  34967  erdszelem9  35167  resconn  35214  cvmseu  35244  cvmlift2lem12  35282  ex-sategoelel  35389  elmrsubrn  35488  mclsind  35538  r1peuqusdeg1  35611  cgrid2  35967  segconeu  35975  btwncomim  35977  btwnswapid  35981  cgrxfr  36019  btwnxfr  36020  colineardim1  36025  brofs2  36041  brifs2  36042  idinside  36048  endofsegid  36049  btwnconn1lem7  36057  btwnconn1lem11  36061  btwnconn1  36065  segcon2  36069  seglemin  36077  segletr  36078  btwnsegle  36081  colinbtwnle  36082  broutsideof2  36086  broutsideof3  36090  outsidele  36096  fvray  36105  fvline  36108  linerflx1  36113  ellines  36116  ivthALT  36299  weiunpo  36429  poimirlem32  37622  ftc1anc  37671  sdclem1  37713  sstotbnd2  37744  zerdivemp1x  37917  isdrngo2  37928  iscringd  37968  lsmsat  38972  lfladdcl  39035  lflnegcl  39039  lflvscl  39041  lshpkrlem4  39077  lshpkrlem6  39079  ldualgrplem  39109  lduallmodlem  39116  latmassOLD  39193  latm12  39194  latm32  39195  latmrot  39196  latmmdiN  39198  latmmdir  39199  omlfh1N  39222  omlfh3N  39223  cvlexchb1  39294  cvlexch3  39296  cvlexch4N  39297  cvlatexchb1  39298  cvlsupr2  39307  hlatjass  39334  hlatj12  39335  hlatj32  39336  cvratlem  39386  cvrat  39387  atcvrj0  39393  cvrat2  39394  atltcvr  39400  atexchltN  39406  cvrat3  39407  cvrat4  39408  3dimlem3  39426  3dimlem3OLDN  39427  3at  39455  2atneat  39480  llncmp  39487  2at0mat0  39490  2atmat0  39491  lplnnle2at  39506  llncvrlpln  39523  lplncmp  39527  lplnexllnN  39529  2llnjaN  39531  4atlem11  39574  lplncvrlvol  39581  lvolcmp  39582  2atm2atN  39750  elpaddatriN  39768  paddasslem9  39793  paddass  39803  padd12N  39804  paddssw2  39809  paddss  39810  pmodlem2  39812  pmodN  39815  pmapjlln1  39820  atmod1i1  39822  atmod1i2  39824  pexmidlem2N  39936  pexmidlem6N  39940  pl42N  39948  lhpm0atN  39994  lautlt  40056  lautcvr  40057  lautj  40058  lautm  40059  ltrneq2  40113  cdlemc3  40158  cdlemc4  40159  cdlemd1  40163  cdleme1b  40191  cdleme1  40192  cdleme2  40193  cdleme3e  40197  cdlemefr27cl  40368  cdlemefs27cl  40378  cdleme42mN  40452  cdlemftr2  40531  trljco  40705  tgrpgrplem  40714  tendoplass  40748  tendodi1  40749  tendodi2  40750  cdlemk36  40878  erngdvlem3  40955  erngdvlem3-rN  40963  tendospdi1  40985  dvalveclem  40990  dialss  41011  dvhvaddass  41062  dvhopvsca  41067  dvhlveclem  41073  diblss  41135  diclss  41158  dihmeetlem12N  41283  dihmeetlem15N  41286  dihmeetlem16N  41287  dihmeetlem17N  41288  dihmeetlem18N  41289  dihmeetlem19N  41290  dvh4dimN  41412  lpolvN  41451  lclkr  41498  lclkrs  41504  lcfr  41550  aks6d1c1  42075  irrapxlem6  42797  jm2.26lem3  42972  dgrsub2  43106  mpaadgr  43125  mendring  43159  mendlmod  43160  mendassa  43161  nnoeomeqom  43283  omabs2  43303  relexpmulg  43681  iunrelexpmin2  43683  relexpxpmin  43688  neicvgel1  44090  fmuldfeq  45560  stoweidlem43  46020  stoweidlem52  46029  stoweidlem53  46030  stoweidlem56  46033  stoweidlem57  46034  issmfle  46722  issmfgt  46733  issmfge  46747  submodaddmod  47318  fmtnoprmfac1  47527  fmtnoprmfac2  47529  clnbgredg  47801  cycl3grtrilem  47906  grlimgrtrilem1  47954  upgrwlkupwlk  48063  copissgrp  48091  cznrng  48184  funcringcsetcALTV2lem9  48221  funcringcsetclem9ALTV  48244  linccl  48338  lincext1  48378  lincext3  48380  lincresunit2  48402  line  48660  rrxline  48662  itsclc0yqsol  48692  resipos  48897  topdlat  48926  catprs  48934  endmndlem  48938  idmon  48943  idepi  48944  thincmon  49267  thincepi  49268  grptcmon  49418  grptcepi  49419