Theorem simpr1 1192

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 1186	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simpr11  1255  simpr21  1258  simpr31  1261  simp1r1  1267  simp2r1  1273  simp3r1  1279  3anandis  1469  fpr2g  7081  isopolem  7209  fr3nr  7613  suppfnss  7989  frrlem4  8089  frrlem8  8093  frfi  9020  intrnfi  9136  iinfi  9137  eqsup  9176  fisupcl  9189  cnfcomlem  9418  ttrclss  9439  ackbij1lem15  9974  fpwwe2lem4  10374  dedekindle  11122  ico0  13107  elioc2  13124  elico2  13125  elicc2  13126  iccsplit  13199  fseq1p1m1  13312  elfz0ubfz0  13342  hashtpg  14180  swrdsbslen  14358  ccatswrd  14362  wwlktovf1  14653  tanadd  15857  dvds2ln  15979  qredeq  16343  ressress  16939  mreexexlem4d  17337  mreexexd  17338  0catg  17378  2oppccomf  17417  issubc3  17545  fthmon  17624  fuccocl  17663  fucidcl  17664  invfuc  17673  initoeu2lem0  17709  initoeu2lem1  17710  curf2cl  17930  yonedalem4c  17976  yonedalem3  17979  pospo  18044  latjle12  18149  latjlej1  18152  latnlej2  18158  latlem12  18165  latmlem1  18168  latledi  18176  latmlej11  18177  latjass  18182  latj12  18183  latj32  18184  latj13  18185  latj31  18186  latjrot  18187  latjjdi  18190  latjjdir  18191  latdisdlem  18195  prdsmndd  18399  imasmnd2  18403  mndissubm  18427  frmdmnd  18479  grpsubrcan  18637  grpsubadd  18644  grpsubsub  18645  grpaddsubass  18646  grpsubsub4  18649  grpnnncan2  18653  imasgrp2  18671  mulgnndir  18713  mulgnn0dir  18714  mulgdir  18716  mulgnnass  18719  mulgnn0ass  18720  mulgass  18721  mulgsubdir  18724  pwsmulg  18729  issubg2  18751  eqgval  18786  qusgrp  18792  galcan  18891  gacan  18892  oppgmnd  18942  pmtrprfv  19042  pmtr3ncom  19064  psgnunilem3  19085  cmn32  19386  cmn12  19388  abladdsub  19397  mulgnn0di  19408  mulgdi  19409  mulgsubdi  19412  dprdss  19613  dprdz  19614  dprdf1o  19616  dprdsn  19620  dprd2da  19626  ablfac1b  19654  pgpfac1lem5  19663  srgbinomlem2  19758  srgbinom  19762  ringi  19780  prdsringd  19832  imasring  19839  opprring  19854  mulgass3  19860  dvrass  19913  kerf1ghm  19968  subrgunit  20023  issubrg2  20025  abvdiv  20078  islss3  20202  prdslmodd  20212  islmhm2  20281  lspsolv  20386  islbs2  20397  islbs3  20398  lbsextlem4  20404  sralmod  20438  ipdir  20825  ipdi  20826  ipsubdir  20828  ipsubdi  20829  ipass  20831  ipassr  20832  ipassr2  20833  ocvlss  20858  sraassa  21055  psrbagleclOLD  21111  psrbagconOLD  21115  psrgrp  21148  psrlmod  21151  psrring  21161  psrassa  21164  mamudm  21518  matring  21573  matassa  21574  ofco2  21581  mdetunilem1  21742  mdetunilem9  21750  mdetuni0  21751  mdetmul  21753  gsummatr01lem3  21787  iinopn  22032  subbascn  22386  nrmsep2  22488  isnrm3  22491  regsep2  22508  dnsconst  22510  dfconn2  22551  1stcelcls  22593  nllyidm  22621  dislly  22629  upxp  22755  fbasne0  22962  filss  22985  infil  22995  fsubbas  22999  filssufilg  23043  tmdcn2  23221  psmettri  23445  isxmet2d  23461  xmettri  23485  xmetres2  23495  bldisj  23532  blss2ps  23537  blss2  23538  xmstri2  23600  mstri2  23601  xmstri  23602  mstri  23603  xmstri3  23604  mstri3  23605  msrtri  23606  comet  23650  stdbdbl  23654  met2ndci  23659  ngprcan  23747  ngplcan  23748  ngpsubcan  23751  nmtri2  23764  nrgdsdi  23810  nrgdsdir  23811  nlmdsdi  23826  nlmdsdir  23827  blcvx  23942  icccmplem2  23967  pi1grplem  24193  pi1cof  24203  clmpm1dir  24247  cvsdiv  24276  cvsdivcl  24277  cphdivcl  24327  cphsubdir  24353  cphsubdi  24354  cphassr  24357  bcthlem5  24473  rrxcph  24537  volfiniun  24692  volcn  24751  itg1val2  24829  dvconst  25062  dvlip  25138  dvfsumlem4  25174  ftc1a  25182  ulmval  25520  ulmdvlem3  25542  ang180  25945  cvxcl  26115  scvxcvx  26116  sgmmul  26330  logexprlim  26354  dchrabl  26383  motgrp  26885  iscgra1  27152  cgrane1  27154  cgrane2  27155  cgrahl1  27158  cgrahl2  27159  cgracgr  27160  cgratr  27165  cgrabtwn  27168  dfcgra2  27172  sacgr  27173  f1otrge  27214  colinearalglem1  27255  colinearalg  27259  axcgrtr  27264  axlowdimlem16  27306  axeuclidlem  27311  axcontlem7  27319  eengtrkg  27335  eengtrkge  27336  nbfusgrlevtxm2  27726  lfgriswlk  28036  upgrwlkdvde  28084  wwlknbp1  28188  erclwwlktr  28365  erclwwlkntr  28414  frgr2wwlkeqm  28674  numclwwlk1lem2f  28698  numclwwlk5  28731  friendship  28742  grpodivdiv  28881  grpomuldivass  28882  ablodivdiv4  28895  ablonnncan1  28898  nvmdi  28989  dipassr  29187  archiabllem2c  31428  dvrdir  31466  dvrcan5  31469  reofld  31523  eqgvscpbl  31529  qusscaval  31531  quslmod  31533  quslmhm  31534  prmidlc  31603  ssmxidl  31621  drgextlsp  31660  ccfldsrarelvec  31720  pstmfval  31825  tpr2rico  31841  qqhval2lem  31910  qqhvq  31916  issiga  32059  measdivcst  32171  measdivcstALTV  32172  carsggect  32264  signsply0  32509  tgoldbachgtd  32621  bnj149  32834  bnj1118  32943  bnj1128  32949  erdszelem9  33140  resconn  33187  cvmseu  33217  cvmlift2lem12  33255  ex-sategoelel  33362  elmrsubrn  33461  mclsind  33511  xpord3pred  33777  sexp3  33778  nosupbnd1  33896  noinfbnd1lem5  33909  noinfbnd1  33911  ssltss1  33962  cgrid2  34284  segconeu  34292  btwncomim  34294  btwnswapid  34298  cgrxfr  34336  btwnxfr  34337  colineardim1  34342  brofs2  34358  brifs2  34359  idinside  34365  endofsegid  34366  btwnconn1lem7  34374  btwnconn1lem11  34378  btwnconn1  34382  segcon2  34386  seglemin  34394  segletr  34395  btwnsegle  34398  colinbtwnle  34399  broutsideof2  34403  broutsideof3  34407  outsidele  34413  fvray  34422  fvline  34425  linerflx1  34430  ellines  34433  ivthALT  34503  poimirlem32  35788  ftc1anc  35837  sdclem1  35880  sstotbnd2  35911  zerdivemp1x  36084  isdrngo2  36095  iscringd  36135  lsmsat  37001  lfladdcl  37064  lflnegcl  37068  lflvscl  37070  lshpkrlem4  37106  lshpkrlem6  37108  ldualgrplem  37138  lduallmodlem  37145  latmassOLD  37222  latm12  37223  latm32  37224  latmrot  37225  latmmdiN  37227  latmmdir  37228  omlfh1N  37251  omlfh3N  37252  cvlexchb1  37323  cvlexch3  37325  cvlexch4N  37326  cvlatexchb1  37327  cvlsupr2  37336  hlatjass  37363  hlatj12  37364  hlatj32  37365  cvratlem  37414  cvrat  37415  atcvrj0  37421  cvrat2  37422  atltcvr  37428  atexchltN  37434  cvrat3  37435  cvrat4  37436  3dimlem3  37454  3dimlem3OLDN  37455  3at  37483  2atneat  37508  llncmp  37515  2at0mat0  37518  2atmat0  37519  lplnnle2at  37534  llncvrlpln  37551  lplncmp  37555  lplnexllnN  37557  2llnjaN  37559  4atlem11  37602  lplncvrlvol  37609  lvolcmp  37610  2atm2atN  37778  elpaddatriN  37796  paddasslem9  37821  paddass  37831  padd12N  37832  paddssw2  37837  paddss  37838  pmodlem2  37840  pmodN  37843  pmapjlln1  37848  atmod1i1  37850  atmod1i2  37852  pexmidlem2N  37964  pexmidlem6N  37968  pl42N  37976  lhpm0atN  38022  lautlt  38084  lautcvr  38085  lautj  38086  lautm  38087  ltrneq2  38141  cdlemc3  38186  cdlemc4  38187  cdlemd1  38191  cdleme1b  38219  cdleme1  38220  cdleme2  38221  cdleme3e  38225  cdlemefr27cl  38396  cdlemefs27cl  38406  cdleme42mN  38480  cdlemftr2  38559  trljco  38733  tgrpgrplem  38742  tendoplass  38776  tendodi1  38777  tendodi2  38778  cdlemk36  38906  erngdvlem3  38983  erngdvlem3-rN  38991  tendospdi1  39013  dvalveclem  39018  dialss  39039  dvhvaddass  39090  dvhopvsca  39095  dvhlveclem  39101  diblss  39163  diclss  39186  dihmeetlem12N  39311  dihmeetlem15N  39314  dihmeetlem16N  39315  dihmeetlem17N  39316  dihmeetlem18N  39317  dihmeetlem19N  39318  dvh4dimN  39440  lpolvN  39479  lclkr  39526  lclkrs  39532  lcfr  39578  irrapxlem6  40629  jm2.26lem3  40803  dgrsub2  40940  mpaadgr  40959  mendring  40997  mendlmod  40998  mendassa  40999  relexpmulg  41271  iunrelexpmin2  41273  relexpxpmin  41278  neicvgel1  41682  fmuldfeq  43078  stoweidlem43  43538  stoweidlem52  43547  stoweidlem53  43548  stoweidlem56  43551  stoweidlem57  43552  issmfle  44232  issmfgt  44243  issmfge  44256  fmtnoprmfac1  44969  fmtnoprmfac2  44971  upgrwlkupwlk  45254  copissgrp  45314  cznrng  45465  funcringcsetcALTV2lem9  45554  funcringcsetclem9ALTV  45577  ply1ass23l  45675  linccl  45707  lincext1  45747  lincext3  45749  lincresunit2  45771  line  46030  rrxline  46032  itsclc0yqsol  46062  topdlat  46242  catprs  46244  endmndlem  46248  idmon  46249  idepi  46250  thincmon  46267  thincepi  46268  grptcmon  46329  grptcepi  46330