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  7145  isopolem  7279  fr3nr  7705  sexp3  8083  suppfnss  8119  frrlem4  8219  frrlem8  8223  dif1en  9071  frfi  9169  intrnfi  9300  iinfi  9301  eqsup  9340  fisupcl  9354  cnfcomlem  9589  ttrclss  9610  ackbij1lem15  10121  fpwwe2lem4  10522  dedekindle  11274  ico0  13288  elioc2  13306  elico2  13307  elicc2  13308  iccsplit  13382  fseq1p1m1  13495  elfz0ubfz0  13529  hashtpg  14389  hash7g  14390  swrdsbslen  14569  ccatswrd  14573  wwlktovf1  14861  tanadd  16073  dvds2ln  16197  qredeq  16565  ressress  17155  mreexexlem4d  17550  mreexexd  17551  0catg  17591  2oppccomf  17628  issubc3  17753  fthmon  17833  fuccocl  17871  fucidcl  17872  invfuc  17881  initoeu2lem0  17917  initoeu2lem1  17918  curf2cl  18134  yonedalem4c  18180  yonedalem3  18183  pospo  18246  latjle12  18353  latjlej1  18356  latnlej2  18362  latlem12  18369  latmlem1  18372  latledi  18380  latmlej11  18381  latjass  18386  latj12  18387  latj32  18388  latj13  18389  latj31  18390  latjrot  18391  latjjdi  18394  latjjdir  18395  latdisdlem  18399  prdssgrpd  18638  prdsmndd  18675  imasmnd2  18679  mndissubm  18712  frmdmnd  18764  grpsubrcan  18931  grpsubadd  18938  grpsubsub  18939  grpaddsubass  18940  grpsubsub4  18943  grpnnncan2  18947  imasgrp2  18965  mulgnndir  19013  mulgnn0dir  19014  mulgdir  19016  mulgnnass  19019  mulgnn0ass  19020  mulgass  19021  mulgsubdir  19024  pwsmulg  19029  issubg2  19051  eqgval  19087  qusgrp  19096  kerf1ghm  19157  galcan  19214  gacan  19215  oppgmnd  19264  pmtrprfv  19363  pmtr3ncom  19385  psgnunilem3  19406  cmn32  19710  cmn12  19712  abladdsub  19722  ablsubaddsub  19724  mulgnn0di  19735  mulgdi  19736  mulgsubdi  19739  dprdss  19941  dprdz  19942  dprdf1o  19944  dprdsn  19948  dprd2da  19954  ablfac1b  19982  pgpfac1lem5  19991  prdsrngd  20092  imasrng  20093  srgbinomlem2  20143  srgbinom  20147  ringdilem  20165  prdsringd  20237  imasring  20246  opprrng  20261  mulgass3  20269  dvrass  20324  dvrdir  20328  subrgunit  20503  issubrg2  20505  abvdiv  20742  islss3  20890  prdslmodd  20900  islmhm2  20970  lspsolv  21078  islbs2  21089  islbs3  21090  lbsextlem4  21096  sralmod  21119  ipdir  21574  ipdi  21575  ipsubdir  21577  ipsubdi  21578  ipass  21580  ipassr  21581  ipassr2  21582  ocvlss  21607  sraassaOLD  21805  psrgrpOLD  21892  psrlmod  21895  psrring  21905  psrassa  21908  ply1ass23l  22137  mamudm  22308  matring  22356  matassa  22357  ofco2  22364  mdetunilem1  22525  mdetunilem9  22533  mdetuni0  22534  mdetmul  22536  gsummatr01lem3  22570  iinopn  22815  subbascn  23167  nrmsep2  23269  isnrm3  23272  regsep2  23289  dnsconst  23291  dfconn2  23332  1stcelcls  23374  nllyidm  23402  dislly  23410  upxp  23536  fbasne0  23743  filss  23766  infil  23776  fsubbas  23780  filssufilg  23824  tmdcn2  24002  psmettri  24224  isxmet2d  24240  xmettri  24264  xmetres2  24274  bldisj  24311  blss2ps  24316  blss2  24317  xmstri2  24379  mstri2  24380  xmstri  24381  mstri  24382  xmstri3  24383  mstri3  24384  msrtri  24385  comet  24426  stdbdbl  24430  met2ndci  24435  ngprcan  24523  ngplcan  24524  ngpsubcan  24527  nmtri2  24540  nrgdsdi  24578  nrgdsdir  24579  nlmdsdi  24594  nlmdsdir  24595  blcvx  24711  icccmplem2  24737  pi1grplem  24974  pi1cof  24984  clmpm1dir  25028  cvsdiv  25057  cvsdivcl  25058  cphdivcl  25107  cphsubdir  25133  cphsubdi  25134  cphassr  25137  bcthlem5  25253  rrxcph  25317  volfiniun  25473  volcn  25532  itg1val2  25610  dvconst  25843  dvlip  25923  dvfsumlem4  25961  ftc1a  25969  ulmval  26314  ulmdvlem3  26336  ang180  26749  cvxcl  26920  scvxcvx  26921  sgmmul  27137  logexprlim  27161  dchrabl  27190  nosupbnd1  27651  noinfbnd1lem5  27664  noinfbnd1  27666  ssltss1  27726  motgrp  28519  iscgra1  28786  cgrane1  28788  cgrane2  28789  cgrahl1  28792  cgrahl2  28793  cgracgr  28794  cgratr  28799  cgrabtwn  28802  dfcgra2  28806  sacgr  28807  f1otrge  28848  colinearalglem1  28882  colinearalg  28886  axcgrtr  28891  axlowdimlem16  28933  axeuclidlem  28938  axcontlem7  28946  eengtrkg  28962  eengtrkge  28963  nbfusgrlevtxm2  29354  lfgriswlk  29663  upgrwlkdvde  29713  wwlknbp1  29820  erclwwlktr  29997  erclwwlkntr  30046  frgr2wwlkeqm  30306  numclwwlk1lem2f  30330  numclwwlk5  30363  friendship  30374  grpodivdiv  30515  grpomuldivass  30516  ablodivdiv4  30529  ablonnncan1  30532  nvmdi  30623  dipassr  30821  archiabllem2c  33159  dvrcan5  33198  rloccring  33232  reofld  33303  eqgvscpbl  33310  qusvsval  33312  quslmod  33318  quslmhm  33319  dvdsruasso2  33346  prmidlc  33408  ssdifidl  33417  ssmxidl  33434  ply1degltlss  33552  r1plmhm  33565  drgextlsp  33601  ccfldsrarelvec  33679  constrconj  33753  constrfin  33754  constrelextdg2  33755  pstmfval  33904  tpr2rico  33920  qqhval2lem  33989  qqhvq  33995  issiga  34120  measdivcst  34232  measdivcstALTV  34233  carsggect  34326  signsply0  34559  tgoldbachgtd  34670  bnj149  34882  bnj1118  34991  bnj1128  34997  erdszelem9  35231  resconn  35278  cvmseu  35308  cvmlift2lem12  35346  ex-sategoelel  35453  elmrsubrn  35552  mclsind  35602  r1peuqusdeg1  35675  cgrid2  36036  segconeu  36044  btwncomim  36046  btwnswapid  36050  cgrxfr  36088  btwnxfr  36089  colineardim1  36094  brofs2  36110  brifs2  36111  idinside  36117  endofsegid  36118  btwnconn1lem7  36126  btwnconn1lem11  36130  btwnconn1  36134  segcon2  36138  seglemin  36146  segletr  36147  btwnsegle  36150  colinbtwnle  36151  broutsideof2  36155  broutsideof3  36159  outsidele  36165  fvray  36174  fvline  36177  linerflx1  36182  ellines  36185  ivthALT  36368  weiunpo  36498  poimirlem32  37691  ftc1anc  37740  sdclem1  37782  sstotbnd2  37813  zerdivemp1x  37986  isdrngo2  37997  iscringd  38037  lsmsat  39046  lfladdcl  39109  lflnegcl  39113  lflvscl  39115  lshpkrlem4  39151  lshpkrlem6  39153  ldualgrplem  39183  lduallmodlem  39190  latmassOLD  39267  latm12  39268  latm32  39269  latmrot  39270  latmmdiN  39272  latmmdir  39273  omlfh1N  39296  omlfh3N  39297  cvlexchb1  39368  cvlexch3  39370  cvlexch4N  39371  cvlatexchb1  39372  cvlsupr2  39381  hlatjass  39408  hlatj12  39409  hlatj32  39410  cvratlem  39459  cvrat  39460  atcvrj0  39466  cvrat2  39467  atltcvr  39473  atexchltN  39479  cvrat3  39480  cvrat4  39481  3dimlem3  39499  3dimlem3OLDN  39500  3at  39528  2atneat  39553  llncmp  39560  2at0mat0  39563  2atmat0  39564  lplnnle2at  39579  llncvrlpln  39596  lplncmp  39600  lplnexllnN  39602  2llnjaN  39604  4atlem11  39647  lplncvrlvol  39654  lvolcmp  39655  2atm2atN  39823  elpaddatriN  39841  paddasslem9  39866  paddass  39876  padd12N  39877  paddssw2  39882  paddss  39883  pmodlem2  39885  pmodN  39888  pmapjlln1  39893  atmod1i1  39895  atmod1i2  39897  pexmidlem2N  40009  pexmidlem6N  40013  pl42N  40021  lhpm0atN  40067  lautlt  40129  lautcvr  40130  lautj  40131  lautm  40132  ltrneq2  40186  cdlemc3  40231  cdlemc4  40232  cdlemd1  40236  cdleme1b  40264  cdleme1  40265  cdleme2  40266  cdleme3e  40270  cdlemefr27cl  40441  cdlemefs27cl  40451  cdleme42mN  40525  cdlemftr2  40604  trljco  40778  tgrpgrplem  40787  tendoplass  40821  tendodi1  40822  tendodi2  40823  cdlemk36  40951  erngdvlem3  41028  erngdvlem3-rN  41036  tendospdi1  41058  dvalveclem  41063  dialss  41084  dvhvaddass  41135  dvhopvsca  41140  dvhlveclem  41146  diblss  41208  diclss  41231  dihmeetlem12N  41356  dihmeetlem15N  41359  dihmeetlem16N  41360  dihmeetlem17N  41361  dihmeetlem18N  41362  dihmeetlem19N  41363  dvh4dimN  41485  lpolvN  41524  lclkr  41571  lclkrs  41577  lcfr  41623  aks6d1c1  42148  irrapxlem6  42859  jm2.26lem3  43033  dgrsub2  43167  mpaadgr  43186  mendring  43220  mendlmod  43221  mendassa  43222  nnoeomeqom  43344  omabs2  43364  relexpmulg  43742  iunrelexpmin2  43744  relexpxpmin  43749  neicvgel1  44151  fmuldfeq  45622  stoweidlem43  46080  stoweidlem52  46089  stoweidlem53  46090  stoweidlem56  46093  stoweidlem57  46094  issmfle  46782  issmfgt  46793  issmfge  46807  submodaddmod  47371  fmtnoprmfac1  47595  fmtnoprmfac2  47597  clnbgredg  47870  cycl3grtrilem  47976  grlimprclnbgr  48026  grlimprclnbgredg  48027  upgrwlkupwlk  48170  copissgrp  48198  cznrng  48291  funcringcsetcALTV2lem9  48328  funcringcsetclem9ALTV  48351  linccl  48445  lincext1  48485  lincext3  48487  lincresunit2  48509  line  48763  rrxline  48765  itsclc0yqsol  48795  resipos  49005  topdlat  49034  catprs  49042  endmndlem  49046  idmon  49051  idepi  49052  thincmon  49464  thincepi  49465  grptcmon  49624  grptcepi  49625