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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simpr11  1258  simpr21  1261  simpr31  1264  simp1r1  1270  simp2r1  1276  simp3r1  1282  3anandis  1472  fpr2g  7213  isopolem  7342  fr3nr  7759  sexp3  8139  suppfnss  8174  frrlem4  8274  frrlem8  8278  dif1en  9160  frfi  9288  intrnfi  9411  iinfi  9412  eqsup  9451  fisupcl  9464  cnfcomlem  9694  ttrclss  9715  ackbij1lem15  10229  fpwwe2lem4  10629  dedekindle  11378  ico0  13370  elioc2  13387  elico2  13388  elicc2  13389  iccsplit  13462  fseq1p1m1  13575  elfz0ubfz0  13605  hashtpg  14446  swrdsbslen  14614  ccatswrd  14618  wwlktovf1  14908  tanadd  16110  dvds2ln  16232  qredeq  16594  ressress  17193  mreexexlem4d  17591  mreexexd  17592  0catg  17632  2oppccomf  17671  issubc3  17799  fthmon  17878  fuccocl  17917  fucidcl  17918  invfuc  17927  initoeu2lem0  17963  initoeu2lem1  17964  curf2cl  18184  yonedalem4c  18230  yonedalem3  18233  pospo  18298  latjle12  18403  latjlej1  18406  latnlej2  18412  latlem12  18419  latmlem1  18422  latledi  18430  latmlej11  18431  latjass  18436  latj12  18437  latj32  18438  latj13  18439  latj31  18440  latjrot  18441  latjjdi  18444  latjjdir  18445  latdisdlem  18449  prdssgrpd  18624  prdsmndd  18658  imasmnd2  18662  mndissubm  18688  frmdmnd  18740  grpsubrcan  18904  grpsubadd  18911  grpsubsub  18912  grpaddsubass  18913  grpsubsub4  18916  grpnnncan2  18920  imasgrp2  18938  mulgnndir  18983  mulgnn0dir  18984  mulgdir  18986  mulgnnass  18989  mulgnn0ass  18990  mulgass  18991  mulgsubdir  18994  pwsmulg  18999  issubg2  19021  eqgval  19057  qusgrp  19065  galcan  19168  gacan  19169  oppgmnd  19221  pmtrprfv  19321  pmtr3ncom  19343  psgnunilem3  19364  cmn32  19668  cmn12  19670  abladdsub  19680  ablsubaddsub  19682  mulgnn0di  19693  mulgdi  19694  mulgsubdi  19697  dprdss  19899  dprdz  19900  dprdf1o  19902  dprdsn  19906  dprd2da  19912  ablfac1b  19940  pgpfac1lem5  19949  srgbinomlem2  20050  srgbinom  20054  ringdilem  20072  prdsringd  20134  imasring  20143  opprring  20161  mulgass3  20167  dvrass  20222  dvrdir  20226  kerf1ghm  20282  subrgunit  20337  issubrg2  20339  abvdiv  20445  islss3  20570  prdslmodd  20580  islmhm2  20649  lspsolv  20756  islbs2  20767  islbs3  20768  lbsextlem4  20774  sralmod  20809  ipdir  21192  ipdi  21193  ipsubdir  21195  ipsubdi  21196  ipass  21198  ipassr  21199  ipassr2  21200  ocvlss  21225  sraassaOLD  21424  psrbagleclOLD  21480  psrbagconOLD  21484  psrgrpOLD  21518  psrlmod  21521  psrring  21531  psrassa  21534  mamudm  21890  matring  21945  matassa  21946  ofco2  21953  mdetunilem1  22114  mdetunilem9  22122  mdetuni0  22123  mdetmul  22125  gsummatr01lem3  22159  iinopn  22404  subbascn  22758  nrmsep2  22860  isnrm3  22863  regsep2  22880  dnsconst  22882  dfconn2  22923  1stcelcls  22965  nllyidm  22993  dislly  23001  upxp  23127  fbasne0  23334  filss  23357  infil  23367  fsubbas  23371  filssufilg  23415  tmdcn2  23593  psmettri  23817  isxmet2d  23833  xmettri  23857  xmetres2  23867  bldisj  23904  blss2ps  23909  blss2  23910  xmstri2  23972  mstri2  23973  xmstri  23974  mstri  23975  xmstri3  23976  mstri3  23977  msrtri  23978  comet  24022  stdbdbl  24026  met2ndci  24031  ngprcan  24119  ngplcan  24120  ngpsubcan  24123  nmtri2  24136  nrgdsdi  24182  nrgdsdir  24183  nlmdsdi  24198  nlmdsdir  24199  blcvx  24314  icccmplem2  24339  pi1grplem  24565  pi1cof  24575  clmpm1dir  24619  cvsdiv  24648  cvsdivcl  24649  cphdivcl  24699  cphsubdir  24725  cphsubdi  24726  cphassr  24729  bcthlem5  24845  rrxcph  24909  volfiniun  25064  volcn  25123  itg1val2  25201  dvconst  25434  dvlip  25510  dvfsumlem4  25546  ftc1a  25554  ulmval  25892  ulmdvlem3  25914  ang180  26319  cvxcl  26489  scvxcvx  26490  sgmmul  26704  logexprlim  26728  dchrabl  26757  nosupbnd1  27217  noinfbnd1lem5  27230  noinfbnd1  27232  ssltss1  27290  motgrp  27825  iscgra1  28092  cgrane1  28094  cgrane2  28095  cgrahl1  28098  cgrahl2  28099  cgracgr  28100  cgratr  28105  cgrabtwn  28108  dfcgra2  28112  sacgr  28113  f1otrge  28154  colinearalglem1  28195  colinearalg  28199  axcgrtr  28204  axlowdimlem16  28246  axeuclidlem  28251  axcontlem7  28259  eengtrkg  28275  eengtrkge  28276  nbfusgrlevtxm2  28666  lfgriswlk  28976  upgrwlkdvde  29025  wwlknbp1  29129  erclwwlktr  29306  erclwwlkntr  29355  frgr2wwlkeqm  29615  numclwwlk1lem2f  29639  numclwwlk5  29672  friendship  29683  grpodivdiv  29824  grpomuldivass  29825  ablodivdiv4  29838  ablonnncan1  29841  nvmdi  29932  dipassr  30130  archiabllem2c  32372  dvrcan5  32416  reofld  32490  eqgvscpbl  32496  qusvsval  32498  quslmod  32500  quslmhm  32501  prmidlc  32598  ssmxidl  32621  ply1degltlss  32698  drgextlsp  32712  ccfldsrarelvec  32776  pstmfval  32907  tpr2rico  32923  qqhval2lem  32992  qqhvq  32998  issiga  33141  measdivcst  33253  measdivcstALTV  33254  carsggect  33348  signsply0  33593  tgoldbachgtd  33705  bnj149  33917  bnj1118  34026  bnj1128  34032  erdszelem9  34221  resconn  34268  cvmseu  34298  cvmlift2lem12  34336  ex-sategoelel  34443  elmrsubrn  34542  mclsind  34592  cgrid2  35006  segconeu  35014  btwncomim  35016  btwnswapid  35020  cgrxfr  35058  btwnxfr  35059  colineardim1  35064  brofs2  35080  brifs2  35081  idinside  35087  endofsegid  35088  btwnconn1lem7  35096  btwnconn1lem11  35100  btwnconn1  35104  segcon2  35108  seglemin  35116  segletr  35117  btwnsegle  35120  colinbtwnle  35121  broutsideof2  35125  broutsideof3  35129  outsidele  35135  fvray  35144  fvline  35147  linerflx1  35152  ellines  35155  ivthALT  35268  poimirlem32  36568  ftc1anc  36617  sdclem1  36659  sstotbnd2  36690  zerdivemp1x  36863  isdrngo2  36874  iscringd  36914  lsmsat  37926  lfladdcl  37989  lflnegcl  37993  lflvscl  37995  lshpkrlem4  38031  lshpkrlem6  38033  ldualgrplem  38063  lduallmodlem  38070  latmassOLD  38147  latm12  38148  latm32  38149  latmrot  38150  latmmdiN  38152  latmmdir  38153  omlfh1N  38176  omlfh3N  38177  cvlexchb1  38248  cvlexch3  38250  cvlexch4N  38251  cvlatexchb1  38252  cvlsupr2  38261  hlatjass  38288  hlatj12  38289  hlatj32  38290  cvratlem  38340  cvrat  38341  atcvrj0  38347  cvrat2  38348  atltcvr  38354  atexchltN  38360  cvrat3  38361  cvrat4  38362  3dimlem3  38380  3dimlem3OLDN  38381  3at  38409  2atneat  38434  llncmp  38441  2at0mat0  38444  2atmat0  38445  lplnnle2at  38460  llncvrlpln  38477  lplncmp  38481  lplnexllnN  38483  2llnjaN  38485  4atlem11  38528  lplncvrlvol  38535  lvolcmp  38536  2atm2atN  38704  elpaddatriN  38722  paddasslem9  38747  paddass  38757  padd12N  38758  paddssw2  38763  paddss  38764  pmodlem2  38766  pmodN  38769  pmapjlln1  38774  atmod1i1  38776  atmod1i2  38778  pexmidlem2N  38890  pexmidlem6N  38894  pl42N  38902  lhpm0atN  38948  lautlt  39010  lautcvr  39011  lautj  39012  lautm  39013  ltrneq2  39067  cdlemc3  39112  cdlemc4  39113  cdlemd1  39117  cdleme1b  39145  cdleme1  39146  cdleme2  39147  cdleme3e  39151  cdlemefr27cl  39322  cdlemefs27cl  39332  cdleme42mN  39406  cdlemftr2  39485  trljco  39659  tgrpgrplem  39668  tendoplass  39702  tendodi1  39703  tendodi2  39704  cdlemk36  39832  erngdvlem3  39909  erngdvlem3-rN  39917  tendospdi1  39939  dvalveclem  39944  dialss  39965  dvhvaddass  40016  dvhopvsca  40021  dvhlveclem  40027  diblss  40089  diclss  40112  dihmeetlem12N  40237  dihmeetlem15N  40240  dihmeetlem16N  40241  dihmeetlem17N  40242  dihmeetlem18N  40243  dihmeetlem19N  40244  dvh4dimN  40366  lpolvN  40405  lclkr  40452  lclkrs  40458  lcfr  40504  irrapxlem6  41613  jm2.26lem3  41788  dgrsub2  41925  mpaadgr  41944  mendring  41982  mendlmod  41983  mendassa  41984  nnoeomeqom  42110  omabs2  42130  relexpmulg  42509  iunrelexpmin2  42511  relexpxpmin  42516  neicvgel1  42918  fmuldfeq  44347  stoweidlem43  44807  stoweidlem52  44816  stoweidlem53  44817  stoweidlem56  44820  stoweidlem57  44821  issmfle  45509  issmfgt  45520  issmfge  45534  fmtnoprmfac1  46281  fmtnoprmfac2  46283  upgrwlkupwlk  46566  copissgrp  46626  opprrng  46722  prdsrngd  46725  imasrng  46726  cznrng  46901  funcringcsetcALTV2lem9  46990  funcringcsetclem9ALTV  47013  ply1ass23l  47111  linccl  47143  lincext1  47183  lincext3  47185  lincresunit2  47207  line  47466  rrxline  47468  itsclc0yqsol  47498  topdlat  47677  catprs  47679  endmndlem  47683  idmon  47684  idepi  47685  thincmon  47702  thincepi  47703  grptcmon  47764  grptcepi  47765