Theorem simpr1 1194

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 1188	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  1257  simpr21  1260  simpr31  1263  simp1r1  1269  simp2r1  1275  simp3r1  1281  3anandis  1471  fpr2g  7248  isopolem  7381  fr3nr  7807  sexp3  8194  suppfnss  8230  frrlem4  8330  frrlem8  8334  dif1en  9226  frfi  9349  intrnfi  9485  iinfi  9486  eqsup  9525  fisupcl  9538  cnfcomlem  9768  ttrclss  9789  ackbij1lem15  10302  fpwwe2lem4  10703  dedekindle  11454  ico0  13453  elioc2  13470  elico2  13471  elicc2  13472  iccsplit  13545  fseq1p1m1  13658  elfz0ubfz0  13689  hashtpg  14534  hash7g  14535  swrdsbslen  14712  ccatswrd  14716  wwlktovf1  15006  tanadd  16215  dvds2ln  16337  qredeq  16704  ressress  17307  mreexexlem4d  17705  mreexexd  17706  0catg  17746  2oppccomf  17785  issubc3  17913  fthmon  17994  fuccocl  18034  fucidcl  18035  invfuc  18044  initoeu2lem0  18080  initoeu2lem1  18081  curf2cl  18301  yonedalem4c  18347  yonedalem3  18350  pospo  18415  latjle12  18520  latjlej1  18523  latnlej2  18529  latlem12  18536  latmlem1  18539  latledi  18547  latmlej11  18548  latjass  18553  latj12  18554  latj32  18555  latj13  18556  latj31  18557  latjrot  18558  latjjdi  18561  latjjdir  18562  latdisdlem  18566  prdssgrpd  18771  prdsmndd  18805  imasmnd2  18809  mndissubm  18842  frmdmnd  18894  grpsubrcan  19061  grpsubadd  19068  grpsubsub  19069  grpaddsubass  19070  grpsubsub4  19073  grpnnncan2  19077  imasgrp2  19095  mulgnndir  19143  mulgnn0dir  19144  mulgdir  19146  mulgnnass  19149  mulgnn0ass  19150  mulgass  19151  mulgsubdir  19154  pwsmulg  19159  issubg2  19181  eqgval  19217  qusgrp  19226  kerf1ghm  19287  galcan  19344  gacan  19345  oppgmnd  19397  pmtrprfv  19495  pmtr3ncom  19517  psgnunilem3  19538  cmn32  19842  cmn12  19844  abladdsub  19854  ablsubaddsub  19856  mulgnn0di  19867  mulgdi  19868  mulgsubdi  19871  dprdss  20073  dprdz  20074  dprdf1o  20076  dprdsn  20080  dprd2da  20086  ablfac1b  20114  pgpfac1lem5  20123  prdsrngd  20203  imasrng  20204  srgbinomlem2  20254  srgbinom  20258  ringdilem  20276  prdsringd  20344  imasring  20353  opprrng  20371  mulgass3  20379  dvrass  20434  dvrdir  20438  subrgunit  20618  issubrg2  20620  abvdiv  20852  islss3  20980  prdslmodd  20990  islmhm2  21060  lspsolv  21168  islbs2  21179  islbs3  21180  lbsextlem4  21186  sralmod  21217  ipdir  21680  ipdi  21681  ipsubdir  21683  ipsubdi  21684  ipass  21686  ipassr  21687  ipassr2  21688  ocvlss  21713  sraassaOLD  21913  psrgrpOLD  22000  psrlmod  22003  psrring  22013  psrassa  22016  ply1ass23l  22249  mamudm  22420  matring  22470  matassa  22471  ofco2  22478  mdetunilem1  22639  mdetunilem9  22647  mdetuni0  22648  mdetmul  22650  gsummatr01lem3  22684  iinopn  22929  subbascn  23283  nrmsep2  23385  isnrm3  23388  regsep2  23405  dnsconst  23407  dfconn2  23448  1stcelcls  23490  nllyidm  23518  dislly  23526  upxp  23652  fbasne0  23859  filss  23882  infil  23892  fsubbas  23896  filssufilg  23940  tmdcn2  24118  psmettri  24342  isxmet2d  24358  xmettri  24382  xmetres2  24392  bldisj  24429  blss2ps  24434  blss2  24435  xmstri2  24497  mstri2  24498  xmstri  24499  mstri  24500  xmstri3  24501  mstri3  24502  msrtri  24503  comet  24547  stdbdbl  24551  met2ndci  24556  ngprcan  24644  ngplcan  24645  ngpsubcan  24648  nmtri2  24661  nrgdsdi  24707  nrgdsdir  24708  nlmdsdi  24723  nlmdsdir  24724  blcvx  24839  icccmplem2  24864  pi1grplem  25101  pi1cof  25111  clmpm1dir  25155  cvsdiv  25184  cvsdivcl  25185  cphdivcl  25235  cphsubdir  25261  cphsubdi  25262  cphassr  25265  bcthlem5  25381  rrxcph  25445  volfiniun  25601  volcn  25660  itg1val2  25738  dvconst  25972  dvlip  26052  dvfsumlem4  26090  ftc1a  26098  ulmval  26441  ulmdvlem3  26463  ang180  26875  cvxcl  27046  scvxcvx  27047  sgmmul  27263  logexprlim  27287  dchrabl  27316  nosupbnd1  27777  noinfbnd1lem5  27790  noinfbnd1  27792  ssltss1  27851  motgrp  28569  iscgra1  28836  cgrane1  28838  cgrane2  28839  cgrahl1  28842  cgrahl2  28843  cgracgr  28844  cgratr  28849  cgrabtwn  28852  dfcgra2  28856  sacgr  28857  f1otrge  28898  colinearalglem1  28939  colinearalg  28943  axcgrtr  28948  axlowdimlem16  28990  axeuclidlem  28995  axcontlem7  29003  eengtrkg  29019  eengtrkge  29020  nbfusgrlevtxm2  29413  lfgriswlk  29724  upgrwlkdvde  29773  wwlknbp1  29877  erclwwlktr  30054  erclwwlkntr  30103  frgr2wwlkeqm  30363  numclwwlk1lem2f  30387  numclwwlk5  30420  friendship  30431  grpodivdiv  30572  grpomuldivass  30573  ablodivdiv4  30586  ablonnncan1  30589  nvmdi  30680  dipassr  30878  archiabllem2c  33175  dvrcan5  33216  rloccring  33242  reofld  33337  eqgvscpbl  33343  qusvsval  33345  quslmod  33351  quslmhm  33352  dvdsruasso2  33379  prmidlc  33441  ssdifidl  33450  ssmxidl  33467  ply1degltlss  33582  r1plmhm  33595  drgextlsp  33608  ccfldsrarelvec  33681  constrconj  33735  constrfin  33736  constrelextdg2  33737  pstmfval  33842  tpr2rico  33858  qqhval2lem  33927  qqhvq  33933  issiga  34076  measdivcst  34188  measdivcstALTV  34189  carsggect  34283  signsply0  34528  tgoldbachgtd  34639  bnj149  34851  bnj1118  34960  bnj1128  34966  erdszelem9  35167  resconn  35214  cvmseu  35244  cvmlift2lem12  35282  ex-sategoelel  35389  elmrsubrn  35488  mclsind  35538  r1peuqusdeg1  35611  cgrid2  35967  segconeu  35975  btwncomim  35977  btwnswapid  35981  cgrxfr  36019  btwnxfr  36020  colineardim1  36025  brofs2  36041  brifs2  36042  idinside  36048  endofsegid  36049  btwnconn1lem7  36057  btwnconn1lem11  36061  btwnconn1  36065  segcon2  36069  seglemin  36077  segletr  36078  btwnsegle  36081  colinbtwnle  36082  broutsideof2  36086  broutsideof3  36090  outsidele  36096  fvray  36105  fvline  36108  linerflx1  36113  ellines  36116  ivthALT  36301  weiunpo  36431  poimirlem32  37612  ftc1anc  37661  sdclem1  37703  sstotbnd2  37734  zerdivemp1x  37907  isdrngo2  37918  iscringd  37958  lsmsat  38964  lfladdcl  39027  lflnegcl  39031  lflvscl  39033  lshpkrlem4  39069  lshpkrlem6  39071  ldualgrplem  39101  lduallmodlem  39108  latmassOLD  39185  latm12  39186  latm32  39187  latmrot  39188  latmmdiN  39190  latmmdir  39191  omlfh1N  39214  omlfh3N  39215  cvlexchb1  39286  cvlexch3  39288  cvlexch4N  39289  cvlatexchb1  39290  cvlsupr2  39299  hlatjass  39326  hlatj12  39327  hlatj32  39328  cvratlem  39378  cvrat  39379  atcvrj0  39385  cvrat2  39386  atltcvr  39392  atexchltN  39398  cvrat3  39399  cvrat4  39400  3dimlem3  39418  3dimlem3OLDN  39419  3at  39447  2atneat  39472  llncmp  39479  2at0mat0  39482  2atmat0  39483  lplnnle2at  39498  llncvrlpln  39515  lplncmp  39519  lplnexllnN  39521  2llnjaN  39523  4atlem11  39566  lplncvrlvol  39573  lvolcmp  39574  2atm2atN  39742  elpaddatriN  39760  paddasslem9  39785  paddass  39795  padd12N  39796  paddssw2  39801  paddss  39802  pmodlem2  39804  pmodN  39807  pmapjlln1  39812  atmod1i1  39814  atmod1i2  39816  pexmidlem2N  39928  pexmidlem6N  39932  pl42N  39940  lhpm0atN  39986  lautlt  40048  lautcvr  40049  lautj  40050  lautm  40051  ltrneq2  40105  cdlemc3  40150  cdlemc4  40151  cdlemd1  40155  cdleme1b  40183  cdleme1  40184  cdleme2  40185  cdleme3e  40189  cdlemefr27cl  40360  cdlemefs27cl  40370  cdleme42mN  40444  cdlemftr2  40523  trljco  40697  tgrpgrplem  40706  tendoplass  40740  tendodi1  40741  tendodi2  40742  cdlemk36  40870  erngdvlem3  40947  erngdvlem3-rN  40955  tendospdi1  40977  dvalveclem  40982  dialss  41003  dvhvaddass  41054  dvhopvsca  41059  dvhlveclem  41065  diblss  41127  diclss  41150  dihmeetlem12N  41275  dihmeetlem15N  41278  dihmeetlem16N  41279  dihmeetlem17N  41280  dihmeetlem18N  41281  dihmeetlem19N  41282  dvh4dimN  41404  lpolvN  41443  lclkr  41490  lclkrs  41496  lcfr  41542  aks6d1c1  42073  irrapxlem6  42783  jm2.26lem3  42958  dgrsub2  43092  mpaadgr  43111  mendring  43149  mendlmod  43150  mendassa  43151  nnoeomeqom  43274  omabs2  43294  relexpmulg  43672  iunrelexpmin2  43674  relexpxpmin  43679  neicvgel1  44081  fmuldfeq  45504  stoweidlem43  45964  stoweidlem52  45973  stoweidlem53  45974  stoweidlem56  45977  stoweidlem57  45978  issmfle  46666  issmfgt  46677  issmfge  46691  fmtnoprmfac1  47439  fmtnoprmfac2  47441  clnbgredg  47712  grlimgrtrilem1  47818  upgrwlkupwlk  47863  copissgrp  47891  cznrng  47984  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  linccl  48143  lincext1  48183  lincext3  48185  lincresunit2  48207  line  48466  rrxline  48468  itsclc0yqsol  48498  topdlat  48676  catprs  48678  endmndlem  48682  idmon  48683  idepi  48684  thincmon  48701  thincepi  48702  grptcmon  48763  grptcepi  48764