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 484	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2antr1 1190	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  1259  simpr21  1262  simpr31  1265  simp1r1  1271  simp2r1  1277  simp3r1  1283  3anandis  1474  fpr2g  7167  isopolem  7301  fr3nr  7727  sexp3  8105  suppfnss  8141  frrlem4  8241  frrlem8  8245  dif1en  9098  frfi  9197  intrnfi  9331  iinfi  9332  eqsup  9371  fisupcl  9385  cnfcomlem  9620  ttrclss  9641  ackbij1lem15  10155  fpwwe2lem4  10557  dedekindle  11309  ico0  13319  elioc2  13337  elico2  13338  elicc2  13339  iccsplit  13413  fseq1p1m1  13526  elfz0ubfz0  13560  hashtpg  14420  hash7g  14421  swrdsbslen  14600  ccatswrd  14604  wwlktovf1  14892  tanadd  16104  dvds2ln  16228  qredeq  16596  ressress  17186  mreexexlem4d  17582  mreexexd  17583  0catg  17623  2oppccomf  17660  issubc3  17785  fthmon  17865  fuccocl  17903  fucidcl  17904  invfuc  17913  initoeu2lem0  17949  initoeu2lem1  17950  curf2cl  18166  yonedalem4c  18212  yonedalem3  18215  pospo  18278  latjle12  18385  latjlej1  18388  latnlej2  18394  latlem12  18401  latmlem1  18404  latledi  18412  latmlej11  18413  latjass  18418  latj12  18419  latj32  18420  latj13  18421  latj31  18422  latjrot  18423  latjjdi  18426  latjjdir  18427  latdisdlem  18431  prdssgrpd  18670  prdsmndd  18707  imasmnd2  18711  mndissubm  18744  frmdmnd  18796  grpsubrcan  18963  grpsubadd  18970  grpsubsub  18971  grpaddsubass  18972  grpsubsub4  18975  grpnnncan2  18979  imasgrp2  18997  mulgnndir  19045  mulgnn0dir  19046  mulgdir  19048  mulgnnass  19051  mulgnn0ass  19052  mulgass  19053  mulgsubdir  19056  pwsmulg  19061  issubg2  19083  eqgval  19118  qusgrp  19127  kerf1ghm  19188  galcan  19245  gacan  19246  oppgmnd  19295  pmtrprfv  19394  pmtr3ncom  19416  psgnunilem3  19437  cmn32  19741  cmn12  19743  abladdsub  19753  ablsubaddsub  19755  mulgnn0di  19766  mulgdi  19767  mulgsubdi  19770  dprdss  19972  dprdz  19973  dprdf1o  19975  dprdsn  19979  dprd2da  19985  ablfac1b  20013  pgpfac1lem5  20022  prdsrngd  20123  imasrng  20124  srgbinomlem2  20174  srgbinom  20178  ringdilem  20196  prdsringd  20268  imasring  20278  opprrng  20293  mulgass3  20301  dvrass  20356  dvrdir  20360  subrgunit  20535  issubrg2  20537  abvdiv  20774  islss3  20922  prdslmodd  20932  islmhm2  21002  lspsolv  21110  islbs2  21121  islbs3  21122  lbsextlem4  21128  sralmod  21151  ipdir  21606  ipdi  21607  ipsubdir  21609  ipsubdi  21610  ipass  21612  ipassr  21613  ipassr2  21614  ocvlss  21639  sraassaOLD  21837  psrlmod  21927  psrring  21937  psrassa  21940  ply1ass23l  22179  mamudm  22351  matring  22399  matassa  22400  ofco2  22407  mdetunilem1  22568  mdetunilem9  22576  mdetuni0  22577  mdetmul  22579  gsummatr01lem3  22613  iinopn  22858  subbascn  23210  nrmsep2  23312  isnrm3  23315  regsep2  23332  dnsconst  23334  dfconn2  23375  1stcelcls  23417  nllyidm  23445  dislly  23453  upxp  23579  fbasne0  23786  filss  23809  infil  23819  fsubbas  23823  filssufilg  23867  tmdcn2  24045  psmettri  24267  isxmet2d  24283  xmettri  24307  xmetres2  24317  bldisj  24354  blss2ps  24359  blss2  24360  xmstri2  24422  mstri2  24423  xmstri  24424  mstri  24425  xmstri3  24426  mstri3  24427  msrtri  24428  comet  24469  stdbdbl  24473  met2ndci  24478  ngprcan  24566  ngplcan  24567  ngpsubcan  24570  nmtri2  24583  nrgdsdi  24621  nrgdsdir  24622  nlmdsdi  24637  nlmdsdir  24638  blcvx  24754  icccmplem2  24780  pi1grplem  25017  pi1cof  25027  clmpm1dir  25071  cvsdiv  25100  cvsdivcl  25101  cphdivcl  25150  cphsubdir  25176  cphsubdi  25177  cphassr  25180  bcthlem5  25296  rrxcph  25360  volfiniun  25516  volcn  25575  itg1val2  25653  dvconst  25886  dvlip  25966  dvfsumlem4  26004  ftc1a  26012  ulmval  26357  ulmdvlem3  26379  ang180  26792  cvxcl  26963  scvxcvx  26964  sgmmul  27180  logexprlim  27204  dchrabl  27233  nosupbnd1  27694  noinfbnd1lem5  27707  noinfbnd1  27709  sltsss1  27773  motgrp  28627  iscgra1  28894  cgrane1  28896  cgrane2  28897  cgrahl1  28900  cgrahl2  28901  cgracgr  28902  cgratr  28907  cgrabtwn  28910  dfcgra2  28914  sacgr  28915  f1otrge  28956  colinearalglem1  28991  colinearalg  28995  axcgrtr  29000  axlowdimlem16  29042  axeuclidlem  29047  axcontlem7  29055  eengtrkg  29071  eengtrkge  29072  nbfusgrlevtxm2  29463  lfgriswlk  29772  upgrwlkdvde  29822  wwlknbp1  29929  usgrwwlks2on  30043  erclwwlktr  30109  erclwwlkntr  30158  frgr2wwlkeqm  30418  numclwwlk1lem2f  30442  numclwwlk5  30475  friendship  30486  grpodivdiv  30627  grpomuldivass  30628  ablodivdiv4  30641  ablonnncan1  30644  nvmdi  30735  dipassr  30933  archiabllem2c  33288  dvrcan5  33329  rloccring  33363  reofld  33435  eqgvscpbl  33442  qusvsval  33444  quslmod  33450  quslmhm  33451  dvdsruasso2  33478  prmidlc  33540  ssdifidl  33549  ssmxidl  33566  ply1degltlss  33688  r1plmhm  33702  drgextlsp  33770  ccfldsrarelvec  33848  constrconj  33922  constrfin  33923  constrelextdg2  33924  pstmfval  34073  tpr2rico  34089  qqhval2lem  34158  qqhvq  34164  issiga  34289  measdivcst  34401  measdivcstALTV  34402  carsggect  34495  signsply0  34728  tgoldbachgtd  34839  bnj149  35050  bnj1118  35159  bnj1128  35165  erdszelem9  35412  resconn  35459  cvmseu  35489  cvmlift2lem12  35527  ex-sategoelel  35634  elmrsubrn  35733  mclsind  35783  r1peuqusdeg1  35856  cgrid2  36216  segconeu  36224  btwncomim  36226  btwnswapid  36230  cgrxfr  36268  btwnxfr  36269  colineardim1  36274  brofs2  36290  brifs2  36291  idinside  36297  endofsegid  36298  btwnconn1lem7  36306  btwnconn1lem11  36310  btwnconn1  36314  segcon2  36318  seglemin  36326  segletr  36327  btwnsegle  36330  colinbtwnle  36331  broutsideof2  36335  broutsideof3  36339  outsidele  36345  fvray  36354  fvline  36357  linerflx1  36362  ellines  36365  ivthALT  36548  weiunpo  36678  poimirlem32  37897  ftc1anc  37946  sdclem1  37988  sstotbnd2  38019  zerdivemp1x  38192  isdrngo2  38203  iscringd  38243  lsmsat  39378  lfladdcl  39441  lflnegcl  39445  lflvscl  39447  lshpkrlem4  39483  lshpkrlem6  39485  ldualgrplem  39515  lduallmodlem  39522  latmassOLD  39599  latm12  39600  latm32  39601  latmrot  39602  latmmdiN  39604  latmmdir  39605  omlfh1N  39628  omlfh3N  39629  cvlexchb1  39700  cvlexch3  39702  cvlexch4N  39703  cvlatexchb1  39704  cvlsupr2  39713  hlatjass  39740  hlatj12  39741  hlatj32  39742  cvratlem  39791  cvrat  39792  atcvrj0  39798  cvrat2  39799  atltcvr  39805  atexchltN  39811  cvrat3  39812  cvrat4  39813  3dimlem3  39831  3dimlem3OLDN  39832  3at  39860  2atneat  39885  llncmp  39892  2at0mat0  39895  2atmat0  39896  lplnnle2at  39911  llncvrlpln  39928  lplncmp  39932  lplnexllnN  39934  2llnjaN  39936  4atlem11  39979  lplncvrlvol  39986  lvolcmp  39987  2atm2atN  40155  elpaddatriN  40173  paddasslem9  40198  paddass  40208  padd12N  40209  paddssw2  40214  paddss  40215  pmodlem2  40217  pmodN  40220  pmapjlln1  40225  atmod1i1  40227  atmod1i2  40229  pexmidlem2N  40341  pexmidlem6N  40345  pl42N  40353  lhpm0atN  40399  lautlt  40461  lautcvr  40462  lautj  40463  lautm  40464  ltrneq2  40518  cdlemc3  40563  cdlemc4  40564  cdlemd1  40568  cdleme1b  40596  cdleme1  40597  cdleme2  40598  cdleme3e  40602  cdlemefr27cl  40773  cdlemefs27cl  40783  cdleme42mN  40857  cdlemftr2  40936  trljco  41110  tgrpgrplem  41119  tendoplass  41153  tendodi1  41154  tendodi2  41155  cdlemk36  41283  erngdvlem3  41360  erngdvlem3-rN  41368  tendospdi1  41390  dvalveclem  41395  dialss  41416  dvhvaddass  41467  dvhopvsca  41472  dvhlveclem  41478  diblss  41540  diclss  41563  dihmeetlem12N  41688  dihmeetlem15N  41691  dihmeetlem16N  41692  dihmeetlem17N  41693  dihmeetlem18N  41694  dihmeetlem19N  41695  dvh4dimN  41817  lpolvN  41856  lclkr  41903  lclkrs  41909  lcfr  41955  aks6d1c1  42480  irrapxlem6  43178  jm2.26lem3  43352  dgrsub2  43486  mpaadgr  43505  mendring  43539  mendlmod  43540  mendassa  43541  nnoeomeqom  43663  omabs2  43683  relexpmulg  44060  iunrelexpmin2  44062  relexpxpmin  44067  neicvgel1  44469  fmuldfeq  45937  stoweidlem43  46395  stoweidlem52  46404  stoweidlem53  46405  stoweidlem56  46408  stoweidlem57  46409  issmfle  47097  issmfgt  47108  issmfge  47122  submodaddmod  47695  fmtnoprmfac1  47919  fmtnoprmfac2  47921  clnbgredg  48194  cycl3grtrilem  48300  grlimprclnbgr  48350  grlimprclnbgredg  48351  upgrwlkupwlk  48494  copissgrp  48522  cznrng  48615  funcringcsetcALTV2lem9  48652  funcringcsetclem9ALTV  48675  linccl  48768  lincext1  48808  lincext3  48810  lincresunit2  48832  line  49086  rrxline  49088  itsclc0yqsol  49118  resipos  49328  topdlat  49357  catprs  49364  endmndlem  49368  idmon  49373  idepi  49374  thincmon  49786  thincepi  49787  grptcmon  49946  grptcepi  49947