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  7151  isopolem  7285  fr3nr  7711  sexp3  8089  suppfnss  8125  frrlem4  8225  frrlem8  8229  dif1en  9078  frfi  9176  intrnfi  9307  iinfi  9308  eqsup  9347  fisupcl  9361  cnfcomlem  9596  ttrclss  9617  ackbij1lem15  10131  fpwwe2lem4  10532  dedekindle  11284  ico0  13293  elioc2  13311  elico2  13312  elicc2  13313  iccsplit  13387  fseq1p1m1  13500  elfz0ubfz0  13534  hashtpg  14394  hash7g  14395  swrdsbslen  14574  ccatswrd  14578  wwlktovf1  14866  tanadd  16078  dvds2ln  16202  qredeq  16570  ressress  17160  mreexexlem4d  17555  mreexexd  17556  0catg  17596  2oppccomf  17633  issubc3  17758  fthmon  17838  fuccocl  17876  fucidcl  17877  invfuc  17886  initoeu2lem0  17922  initoeu2lem1  17923  curf2cl  18139  yonedalem4c  18185  yonedalem3  18188  pospo  18251  latjle12  18358  latjlej1  18361  latnlej2  18367  latlem12  18374  latmlem1  18377  latledi  18385  latmlej11  18386  latjass  18391  latj12  18392  latj32  18393  latj13  18394  latj31  18395  latjrot  18396  latjjdi  18399  latjjdir  18400  latdisdlem  18404  prdssgrpd  18643  prdsmndd  18680  imasmnd2  18684  mndissubm  18717  frmdmnd  18769  grpsubrcan  18936  grpsubadd  18943  grpsubsub  18944  grpaddsubass  18945  grpsubsub4  18948  grpnnncan2  18952  imasgrp2  18970  mulgnndir  19018  mulgnn0dir  19019  mulgdir  19021  mulgnnass  19024  mulgnn0ass  19025  mulgass  19026  mulgsubdir  19029  pwsmulg  19034  issubg2  19056  eqgval  19091  qusgrp  19100  kerf1ghm  19161  galcan  19218  gacan  19219  oppgmnd  19268  pmtrprfv  19367  pmtr3ncom  19389  psgnunilem3  19410  cmn32  19714  cmn12  19716  abladdsub  19726  ablsubaddsub  19728  mulgnn0di  19739  mulgdi  19740  mulgsubdi  19743  dprdss  19945  dprdz  19946  dprdf1o  19948  dprdsn  19952  dprd2da  19958  ablfac1b  19986  pgpfac1lem5  19995  prdsrngd  20096  imasrng  20097  srgbinomlem2  20147  srgbinom  20151  ringdilem  20169  prdsringd  20241  imasring  20250  opprrng  20265  mulgass3  20273  dvrass  20328  dvrdir  20332  subrgunit  20507  issubrg2  20509  abvdiv  20746  islss3  20894  prdslmodd  20904  islmhm2  20974  lspsolv  21082  islbs2  21093  islbs3  21094  lbsextlem4  21100  sralmod  21123  ipdir  21578  ipdi  21579  ipsubdir  21581  ipsubdi  21582  ipass  21584  ipassr  21585  ipassr2  21586  ocvlss  21611  sraassaOLD  21809  psrlmod  21898  psrring  21908  psrassa  21911  ply1ass23l  22140  mamudm  22311  matring  22359  matassa  22360  ofco2  22367  mdetunilem1  22528  mdetunilem9  22536  mdetuni0  22537  mdetmul  22539  gsummatr01lem3  22573  iinopn  22818  subbascn  23170  nrmsep2  23272  isnrm3  23275  regsep2  23292  dnsconst  23294  dfconn2  23335  1stcelcls  23377  nllyidm  23405  dislly  23413  upxp  23539  fbasne0  23746  filss  23769  infil  23779  fsubbas  23783  filssufilg  23827  tmdcn2  24005  psmettri  24227  isxmet2d  24243  xmettri  24267  xmetres2  24277  bldisj  24314  blss2ps  24319  blss2  24320  xmstri2  24382  mstri2  24383  xmstri  24384  mstri  24385  xmstri3  24386  mstri3  24387  msrtri  24388  comet  24429  stdbdbl  24433  met2ndci  24438  ngprcan  24526  ngplcan  24527  ngpsubcan  24530  nmtri2  24543  nrgdsdi  24581  nrgdsdir  24582  nlmdsdi  24597  nlmdsdir  24598  blcvx  24714  icccmplem2  24740  pi1grplem  24977  pi1cof  24987  clmpm1dir  25031  cvsdiv  25060  cvsdivcl  25061  cphdivcl  25110  cphsubdir  25136  cphsubdi  25137  cphassr  25140  bcthlem5  25256  rrxcph  25320  volfiniun  25476  volcn  25535  itg1val2  25613  dvconst  25846  dvlip  25926  dvfsumlem4  25964  ftc1a  25972  ulmval  26317  ulmdvlem3  26339  ang180  26752  cvxcl  26923  scvxcvx  26924  sgmmul  27140  logexprlim  27164  dchrabl  27193  nosupbnd1  27654  noinfbnd1lem5  27667  noinfbnd1  27669  ssltss1  27729  motgrp  28522  iscgra1  28789  cgrane1  28791  cgrane2  28792  cgrahl1  28795  cgrahl2  28796  cgracgr  28797  cgratr  28802  cgrabtwn  28805  dfcgra2  28809  sacgr  28810  f1otrge  28851  colinearalglem1  28886  colinearalg  28890  axcgrtr  28895  axlowdimlem16  28937  axeuclidlem  28942  axcontlem7  28950  eengtrkg  28966  eengtrkge  28967  nbfusgrlevtxm2  29358  lfgriswlk  29667  upgrwlkdvde  29717  wwlknbp1  29824  usgrwwlks2on  29938  erclwwlktr  30004  erclwwlkntr  30053  frgr2wwlkeqm  30313  numclwwlk1lem2f  30337  numclwwlk5  30370  friendship  30381  grpodivdiv  30522  grpomuldivass  30523  ablodivdiv4  30536  ablonnncan1  30539  nvmdi  30630  dipassr  30828  archiabllem2c  33171  dvrcan5  33210  rloccring  33244  reofld  33315  eqgvscpbl  33322  qusvsval  33324  quslmod  33330  quslmhm  33331  dvdsruasso2  33358  prmidlc  33420  ssdifidl  33429  ssmxidl  33446  ply1degltlss  33564  r1plmhm  33577  drgextlsp  33627  ccfldsrarelvec  33705  constrconj  33779  constrfin  33780  constrelextdg2  33781  pstmfval  33930  tpr2rico  33946  qqhval2lem  34015  qqhvq  34021  issiga  34146  measdivcst  34258  measdivcstALTV  34259  carsggect  34352  signsply0  34585  tgoldbachgtd  34696  bnj149  34908  bnj1118  35017  bnj1128  35023  erdszelem9  35264  resconn  35311  cvmseu  35341  cvmlift2lem12  35379  ex-sategoelel  35486  elmrsubrn  35585  mclsind  35635  r1peuqusdeg1  35708  cgrid2  36068  segconeu  36076  btwncomim  36078  btwnswapid  36082  cgrxfr  36120  btwnxfr  36121  colineardim1  36126  brofs2  36142  brifs2  36143  idinside  36149  endofsegid  36150  btwnconn1lem7  36158  btwnconn1lem11  36162  btwnconn1  36166  segcon2  36170  seglemin  36178  segletr  36179  btwnsegle  36182  colinbtwnle  36183  broutsideof2  36187  broutsideof3  36191  outsidele  36197  fvray  36206  fvline  36209  linerflx1  36214  ellines  36217  ivthALT  36400  weiunpo  36530  poimirlem32  37712  ftc1anc  37761  sdclem1  37803  sstotbnd2  37834  zerdivemp1x  38007  isdrngo2  38018  iscringd  38058  lsmsat  39127  lfladdcl  39190  lflnegcl  39194  lflvscl  39196  lshpkrlem4  39232  lshpkrlem6  39234  ldualgrplem  39264  lduallmodlem  39271  latmassOLD  39348  latm12  39349  latm32  39350  latmrot  39351  latmmdiN  39353  latmmdir  39354  omlfh1N  39377  omlfh3N  39378  cvlexchb1  39449  cvlexch3  39451  cvlexch4N  39452  cvlatexchb1  39453  cvlsupr2  39462  hlatjass  39489  hlatj12  39490  hlatj32  39491  cvratlem  39540  cvrat  39541  atcvrj0  39547  cvrat2  39548  atltcvr  39554  atexchltN  39560  cvrat3  39561  cvrat4  39562  3dimlem3  39580  3dimlem3OLDN  39581  3at  39609  2atneat  39634  llncmp  39641  2at0mat0  39644  2atmat0  39645  lplnnle2at  39660  llncvrlpln  39677  lplncmp  39681  lplnexllnN  39683  2llnjaN  39685  4atlem11  39728  lplncvrlvol  39735  lvolcmp  39736  2atm2atN  39904  elpaddatriN  39922  paddasslem9  39947  paddass  39957  padd12N  39958  paddssw2  39963  paddss  39964  pmodlem2  39966  pmodN  39969  pmapjlln1  39974  atmod1i1  39976  atmod1i2  39978  pexmidlem2N  40090  pexmidlem6N  40094  pl42N  40102  lhpm0atN  40148  lautlt  40210  lautcvr  40211  lautj  40212  lautm  40213  ltrneq2  40267  cdlemc3  40312  cdlemc4  40313  cdlemd1  40317  cdleme1b  40345  cdleme1  40346  cdleme2  40347  cdleme3e  40351  cdlemefr27cl  40522  cdlemefs27cl  40532  cdleme42mN  40606  cdlemftr2  40685  trljco  40859  tgrpgrplem  40868  tendoplass  40902  tendodi1  40903  tendodi2  40904  cdlemk36  41032  erngdvlem3  41109  erngdvlem3-rN  41117  tendospdi1  41139  dvalveclem  41144  dialss  41165  dvhvaddass  41216  dvhopvsca  41221  dvhlveclem  41227  diblss  41289  diclss  41312  dihmeetlem12N  41437  dihmeetlem15N  41440  dihmeetlem16N  41441  dihmeetlem17N  41442  dihmeetlem18N  41443  dihmeetlem19N  41444  dvh4dimN  41566  lpolvN  41605  lclkr  41652  lclkrs  41658  lcfr  41704  aks6d1c1  42229  irrapxlem6  42944  jm2.26lem3  43118  dgrsub2  43252  mpaadgr  43271  mendring  43305  mendlmod  43306  mendassa  43307  nnoeomeqom  43429  omabs2  43449  relexpmulg  43827  iunrelexpmin2  43829  relexpxpmin  43834  neicvgel1  44236  fmuldfeq  45707  stoweidlem43  46165  stoweidlem52  46174  stoweidlem53  46175  stoweidlem56  46178  stoweidlem57  46179  issmfle  46867  issmfgt  46878  issmfge  46892  submodaddmod  47465  fmtnoprmfac1  47689  fmtnoprmfac2  47691  clnbgredg  47964  cycl3grtrilem  48070  grlimprclnbgr  48120  grlimprclnbgredg  48121  upgrwlkupwlk  48264  copissgrp  48292  cznrng  48385  funcringcsetcALTV2lem9  48422  funcringcsetclem9ALTV  48445  linccl  48539  lincext1  48579  lincext3  48581  lincresunit2  48603  line  48857  rrxline  48859  itsclc0yqsol  48889  resipos  49099  topdlat  49128  catprs  49136  endmndlem  49140  idmon  49145  idepi  49146  thincmon  49558  thincepi  49559  grptcmon  49718  grptcepi  49719