Theorem simpr1 1196

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  simpr11  1259  simpr21  1262  simpr31  1265  simp1r1  1271  simp2r1  1277  simp3r1  1283  3anandis  1473  fpr2g  7027  isopolem  7154  fr3nr  7557  suppfnss  7931  frrlem4  8030  frrlem8  8034  frfi  8916  intrnfi  9032  iinfi  9033  eqsup  9072  fisupcl  9085  cnfcomlem  9314  ackbij1lem15  9848  fpwwe2lem4  10248  dedekindle  10996  ico0  12981  elioc2  12998  elico2  12999  elicc2  13000  iccsplit  13073  fseq1p1m1  13186  elfz0ubfz0  13216  hashtpg  14051  swrdsbslen  14229  ccatswrd  14233  wwlktovf1  14524  tanadd  15728  dvds2ln  15850  qredeq  16214  ressress  16799  mreexexlem4d  17150  mreexexd  17151  0catg  17191  2oppccomf  17229  issubc3  17355  fthmon  17434  fuccocl  17473  fucidcl  17474  invfuc  17483  initoeu2lem0  17519  initoeu2lem1  17520  curf2cl  17739  yonedalem4c  17785  yonedalem3  17788  pospo  17851  latjle12  17956  latjlej1  17959  latnlej2  17965  latlem12  17972  latmlem1  17975  latledi  17983  latmlej11  17984  latjass  17989  latj12  17990  latj32  17991  latj13  17992  latj31  17993  latjrot  17994  latjjdi  17997  latjjdir  17998  latdisdlem  18002  prdsmndd  18206  imasmnd2  18210  mndissubm  18234  frmdmnd  18286  grpsubrcan  18444  grpsubadd  18451  grpsubsub  18452  grpaddsubass  18453  grpsubsub4  18456  grpnnncan2  18460  imasgrp2  18478  mulgnndir  18520  mulgnn0dir  18521  mulgdir  18523  mulgnnass  18526  mulgnn0ass  18527  mulgass  18528  mulgsubdir  18531  pwsmulg  18536  issubg2  18558  eqgval  18593  qusgrp  18599  galcan  18698  gacan  18699  oppgmnd  18746  pmtrprfv  18845  pmtr3ncom  18867  psgnunilem3  18888  cmn32  19189  cmn12  19191  abladdsub  19200  mulgnn0di  19211  mulgdi  19212  mulgsubdi  19215  dprdss  19416  dprdz  19417  dprdf1o  19419  dprdsn  19423  dprd2da  19429  ablfac1b  19457  pgpfac1lem5  19466  srgbinomlem2  19556  srgbinom  19560  ringi  19578  prdsringd  19630  imasring  19637  opprring  19649  mulgass3  19655  dvrass  19708  kerf1ghm  19763  subrgunit  19818  issubrg2  19820  abvdiv  19873  islss3  19996  prdslmodd  20006  islmhm2  20075  lspsolv  20180  islbs2  20191  islbs3  20192  lbsextlem4  20198  sralmod  20224  ipdir  20601  ipdi  20602  ipsubdir  20604  ipsubdi  20605  ipass  20607  ipassr  20608  ipassr2  20609  ocvlss  20634  sraassa  20829  psrbagleclOLD  20886  psrbagconOLD  20890  psrgrp  20923  psrlmod  20926  psrring  20936  psrassa  20939  mamudm  21287  matring  21340  matassa  21341  ofco2  21348  mdetunilem1  21509  mdetunilem9  21517  mdetuni0  21518  mdetmul  21520  gsummatr01lem3  21554  iinopn  21799  subbascn  22151  nrmsep2  22253  isnrm3  22256  regsep2  22273  dnsconst  22275  dfconn2  22316  1stcelcls  22358  nllyidm  22386  dislly  22394  upxp  22520  fbasne0  22727  filss  22750  infil  22760  fsubbas  22764  filssufilg  22808  tmdcn2  22986  psmettri  23209  isxmet2d  23225  xmettri  23249  xmetres2  23259  bldisj  23296  blss2ps  23301  blss2  23302  xmstri2  23364  mstri2  23365  xmstri  23366  mstri  23367  xmstri3  23368  mstri3  23369  msrtri  23370  comet  23411  stdbdbl  23415  met2ndci  23420  ngprcan  23508  ngplcan  23509  ngpsubcan  23512  nmtri2  23525  nrgdsdi  23563  nrgdsdir  23564  nlmdsdi  23579  nlmdsdir  23580  blcvx  23695  icccmplem2  23720  pi1grplem  23946  pi1cof  23956  clmpm1dir  24000  cvsdiv  24029  cvsdivcl  24030  cphdivcl  24079  cphsubdir  24105  cphsubdi  24106  cphassr  24109  bcthlem5  24225  rrxcph  24289  volfiniun  24444  volcn  24503  itg1val2  24581  dvconst  24814  dvlip  24890  dvfsumlem4  24926  ftc1a  24934  ulmval  25272  ulmdvlem3  25294  ang180  25697  cvxcl  25867  scvxcvx  25868  sgmmul  26082  logexprlim  26106  dchrabl  26135  motgrp  26634  iscgra1  26901  cgrane1  26903  cgrane2  26904  cgrahl1  26907  cgrahl2  26908  cgracgr  26909  cgratr  26914  cgrabtwn  26917  dfcgra2  26921  sacgr  26922  f1otrge  26963  colinearalglem1  26997  colinearalg  27001  axcgrtr  27006  axlowdimlem16  27048  axeuclidlem  27053  axcontlem7  27061  eengtrkg  27077  eengtrkge  27078  nbfusgrlevtxm2  27466  lfgriswlk  27776  upgrwlkdvde  27824  wwlknbp1  27928  erclwwlktr  28105  erclwwlkntr  28154  frgr2wwlkeqm  28414  numclwwlk1lem2f  28438  numclwwlk5  28471  friendship  28482  grpodivdiv  28621  grpomuldivass  28622  ablodivdiv4  28635  ablonnncan1  28638  nvmdi  28729  dipassr  28927  archiabllem2c  31168  dvrdir  31206  dvrcan5  31209  reofld  31258  eqgvscpbl  31264  qusscaval  31266  quslmod  31268  quslmhm  31269  prmidlc  31338  ssmxidl  31356  drgextlsp  31395  ccfldsrarelvec  31455  pstmfval  31560  tpr2rico  31576  qqhval2lem  31643  qqhvq  31649  issiga  31792  measdivcst  31904  measdivcstALTV  31905  carsggect  31997  signsply0  32242  tgoldbachgtd  32354  bnj149  32568  bnj1118  32677  bnj1128  32683  erdszelem9  32874  resconn  32921  cvmseu  32951  cvmlift2lem12  32989  ex-sategoelel  33096  elmrsubrn  33195  mclsind  33245  ttrclss  33519  xpord3pred  33535  sexp3  33536  nosupbnd1  33654  noinfbnd1lem5  33667  noinfbnd1  33669  ssltss1  33720  cgrid2  34042  segconeu  34050  btwncomim  34052  btwnswapid  34056  cgrxfr  34094  btwnxfr  34095  colineardim1  34100  brofs2  34116  brifs2  34117  idinside  34123  endofsegid  34124  btwnconn1lem7  34132  btwnconn1lem11  34136  btwnconn1  34140  segcon2  34144  seglemin  34152  segletr  34153  btwnsegle  34156  colinbtwnle  34157  broutsideof2  34161  broutsideof3  34165  outsidele  34171  fvray  34180  fvline  34183  linerflx1  34188  ellines  34191  ivthALT  34261  poimirlem32  35546  ftc1anc  35595  sdclem1  35638  sstotbnd2  35669  zerdivemp1x  35842  isdrngo2  35853  iscringd  35893  lsmsat  36759  lfladdcl  36822  lflnegcl  36826  lflvscl  36828  lshpkrlem4  36864  lshpkrlem6  36866  ldualgrplem  36896  lduallmodlem  36903  latmassOLD  36980  latm12  36981  latm32  36982  latmrot  36983  latmmdiN  36985  latmmdir  36986  omlfh1N  37009  omlfh3N  37010  cvlexchb1  37081  cvlexch3  37083  cvlexch4N  37084  cvlatexchb1  37085  cvlsupr2  37094  hlatjass  37121  hlatj12  37122  hlatj32  37123  cvratlem  37172  cvrat  37173  atcvrj0  37179  cvrat2  37180  atltcvr  37186  atexchltN  37192  cvrat3  37193  cvrat4  37194  3dimlem3  37212  3dimlem3OLDN  37213  3at  37241  2atneat  37266  llncmp  37273  2at0mat0  37276  2atmat0  37277  lplnnle2at  37292  llncvrlpln  37309  lplncmp  37313  lplnexllnN  37315  2llnjaN  37317  4atlem11  37360  lplncvrlvol  37367  lvolcmp  37368  2atm2atN  37536  elpaddatriN  37554  paddasslem9  37579  paddass  37589  padd12N  37590  paddssw2  37595  paddss  37596  pmodlem2  37598  pmodN  37601  pmapjlln1  37606  atmod1i1  37608  atmod1i2  37610  pexmidlem2N  37722  pexmidlem6N  37726  pl42N  37734  lhpm0atN  37780  lautlt  37842  lautcvr  37843  lautj  37844  lautm  37845  ltrneq2  37899  cdlemc3  37944  cdlemc4  37945  cdlemd1  37949  cdleme1b  37977  cdleme1  37978  cdleme2  37979  cdleme3e  37983  cdlemefr27cl  38154  cdlemefs27cl  38164  cdleme42mN  38238  cdlemftr2  38317  trljco  38491  tgrpgrplem  38500  tendoplass  38534  tendodi1  38535  tendodi2  38536  cdlemk36  38664  erngdvlem3  38741  erngdvlem3-rN  38749  tendospdi1  38771  dvalveclem  38776  dialss  38797  dvhvaddass  38848  dvhopvsca  38853  dvhlveclem  38859  diblss  38921  diclss  38944  dihmeetlem12N  39069  dihmeetlem15N  39072  dihmeetlem16N  39073  dihmeetlem17N  39074  dihmeetlem18N  39075  dihmeetlem19N  39076  dvh4dimN  39198  lpolvN  39237  lclkr  39284  lclkrs  39290  lcfr  39336  irrapxlem6  40352  jm2.26lem3  40526  dgrsub2  40663  mpaadgr  40682  mendring  40720  mendlmod  40721  mendassa  40722  relexpmulg  40995  iunrelexpmin2  40997  relexpxpmin  41002  neicvgel1  41406  fmuldfeq  42799  stoweidlem43  43259  stoweidlem52  43268  stoweidlem53  43269  stoweidlem56  43272  stoweidlem57  43273  issmfle  43953  issmfgt  43964  issmfge  43977  fmtnoprmfac1  44690  fmtnoprmfac2  44692  upgrwlkupwlk  44975  copissgrp  45035  cznrng  45186  funcringcsetcALTV2lem9  45275  funcringcsetclem9ALTV  45298  ply1ass23l  45396  linccl  45428  lincext1  45468  lincext3  45470  lincresunit2  45492  line  45751  rrxline  45753  itsclc0yqsol  45783  topdlat  45963  catprs  45965  endmndlem  45969  idmon  45970  idepi  45971  thincmon  45988  thincepi  45989  grptcmon  46048  grptcepi  46049