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  7159  isopolem  7293  fr3nr  7719  sexp3  8096  suppfnss  8132  frrlem4  8232  frrlem8  8236  dif1en  9089  frfi  9188  intrnfi  9322  iinfi  9323  eqsup  9362  fisupcl  9376  cnfcomlem  9611  ttrclss  9632  ackbij1lem15  10146  fpwwe2lem4  10548  dedekindle  11301  ico0  13335  elioc2  13353  elico2  13354  elicc2  13355  iccsplit  13429  fseq1p1m1  13543  elfz0ubfz0  13577  hashtpg  14438  hash7g  14439  swrdsbslen  14618  ccatswrd  14622  wwlktovf1  14910  tanadd  16125  dvds2ln  16249  qredeq  16617  ressress  17208  mreexexlem4d  17604  mreexexd  17605  0catg  17645  2oppccomf  17682  issubc3  17807  fthmon  17887  fuccocl  17925  fucidcl  17926  invfuc  17935  initoeu2lem0  17971  initoeu2lem1  17972  curf2cl  18188  yonedalem4c  18234  yonedalem3  18237  pospo  18300  latjle12  18407  latjlej1  18410  latnlej2  18416  latlem12  18423  latmlem1  18426  latledi  18434  latmlej11  18435  latjass  18440  latj12  18441  latj32  18442  latj13  18443  latj31  18444  latjrot  18445  latjjdi  18448  latjjdir  18449  latdisdlem  18453  prdssgrpd  18692  prdsmndd  18729  imasmnd2  18733  mndissubm  18766  frmdmnd  18818  grpsubrcan  18988  grpsubadd  18995  grpsubsub  18996  grpaddsubass  18997  grpsubsub4  19000  grpnnncan2  19004  imasgrp2  19022  mulgnndir  19070  mulgnn0dir  19071  mulgdir  19073  mulgnnass  19076  mulgnn0ass  19077  mulgass  19078  mulgsubdir  19081  pwsmulg  19086  issubg2  19108  eqgval  19143  qusgrp  19152  kerf1ghm  19213  galcan  19270  gacan  19271  oppgmnd  19320  pmtrprfv  19419  pmtr3ncom  19441  psgnunilem3  19462  cmn32  19766  cmn12  19768  abladdsub  19778  ablsubaddsub  19780  mulgnn0di  19791  mulgdi  19792  mulgsubdi  19795  dprdss  19997  dprdz  19998  dprdf1o  20000  dprdsn  20004  dprd2da  20010  ablfac1b  20038  pgpfac1lem5  20047  prdsrngd  20148  imasrng  20149  srgbinomlem2  20199  srgbinom  20203  ringdilem  20221  prdsringd  20291  imasring  20301  opprrng  20316  mulgass3  20324  dvrass  20379  dvrdir  20383  subrgunit  20558  issubrg2  20560  abvdiv  20797  islss3  20945  prdslmodd  20955  islmhm2  21025  lspsolv  21133  islbs2  21144  islbs3  21145  lbsextlem4  21151  sralmod  21174  ipdir  21629  ipdi  21630  ipsubdir  21632  ipsubdi  21633  ipass  21635  ipassr  21636  ipassr2  21637  ocvlss  21662  psrlmod  21948  psrring  21958  psrassa  21961  ply1ass23l  22200  mamudm  22370  matring  22418  matassa  22419  ofco2  22426  mdetunilem1  22587  mdetunilem9  22595  mdetuni0  22596  mdetmul  22598  gsummatr01lem3  22632  iinopn  22877  subbascn  23229  nrmsep2  23331  isnrm3  23334  regsep2  23351  dnsconst  23353  dfconn2  23394  1stcelcls  23436  nllyidm  23464  dislly  23472  upxp  23598  fbasne0  23805  filss  23828  infil  23838  fsubbas  23842  filssufilg  23886  tmdcn2  24064  psmettri  24286  isxmet2d  24302  xmettri  24326  xmetres2  24336  bldisj  24373  blss2ps  24378  blss2  24379  xmstri2  24441  mstri2  24442  xmstri  24443  mstri  24444  xmstri3  24445  mstri3  24446  msrtri  24447  comet  24488  stdbdbl  24492  met2ndci  24497  ngprcan  24585  ngplcan  24586  ngpsubcan  24589  nmtri2  24602  nrgdsdi  24640  nrgdsdir  24641  nlmdsdi  24656  nlmdsdir  24657  blcvx  24773  icccmplem2  24799  pi1grplem  25026  pi1cof  25036  clmpm1dir  25080  cvsdiv  25109  cvsdivcl  25110  cphdivcl  25159  cphsubdir  25185  cphsubdi  25186  cphassr  25189  bcthlem5  25305  rrxcph  25369  volfiniun  25524  volcn  25583  itg1val2  25661  dvconst  25894  dvlip  25970  dvfsumlem4  26006  ftc1a  26014  ulmval  26358  ulmdvlem3  26380  ang180  26791  cvxcl  26962  scvxcvx  26963  sgmmul  27178  logexprlim  27202  dchrabl  27231  nosupbnd1  27692  noinfbnd1lem5  27705  noinfbnd1  27707  sltsss1  27771  motgrp  28625  iscgra1  28892  cgrane1  28894  cgrane2  28895  cgrahl1  28898  cgrahl2  28899  cgracgr  28900  cgratr  28905  cgrabtwn  28908  dfcgra2  28912  sacgr  28913  f1otrge  28954  colinearalglem1  28989  colinearalg  28993  axcgrtr  28998  axlowdimlem16  29040  axeuclidlem  29045  axcontlem7  29053  eengtrkg  29069  eengtrkge  29070  nbfusgrlevtxm2  29461  lfgriswlk  29770  upgrwlkdvde  29820  wwlknbp1  29927  usgrwwlks2on  30041  erclwwlktr  30107  erclwwlkntr  30156  frgr2wwlkeqm  30416  numclwwlk1lem2f  30440  numclwwlk5  30473  friendship  30484  grpodivdiv  30626  grpomuldivass  30627  ablodivdiv4  30640  ablonnncan1  30643  nvmdi  30734  dipassr  30932  archiabllem2c  33271  dvrcan5  33312  rloccring  33346  reofld  33418  eqgvscpbl  33425  qusvsval  33427  quslmod  33433  quslmhm  33434  dvdsruasso2  33461  prmidlc  33523  ssdifidl  33532  ssmxidl  33549  ply1degltlss  33671  r1plmhm  33685  drgextlsp  33753  ccfldsrarelvec  33831  constrconj  33905  constrfin  33906  constrelextdg2  33907  pstmfval  34056  tpr2rico  34072  qqhval2lem  34141  qqhvq  34147  issiga  34272  measdivcst  34384  measdivcstALTV  34385  carsggect  34478  signsply0  34711  tgoldbachgtd  34822  bnj149  35033  bnj1118  35142  bnj1128  35148  erdszelem9  35397  resconn  35444  cvmseu  35474  cvmlift2lem12  35512  ex-sategoelel  35619  elmrsubrn  35718  mclsind  35768  r1peuqusdeg1  35841  cgrid2  36201  segconeu  36209  btwncomim  36211  btwnswapid  36215  cgrxfr  36253  btwnxfr  36254  colineardim1  36259  brofs2  36275  brifs2  36276  idinside  36282  endofsegid  36283  btwnconn1lem7  36291  btwnconn1lem11  36295  btwnconn1  36299  segcon2  36303  seglemin  36311  segletr  36312  btwnsegle  36315  colinbtwnle  36316  broutsideof2  36320  broutsideof3  36324  outsidele  36330  fvray  36339  fvline  36342  linerflx1  36347  ellines  36350  ivthALT  36533  weiunpo  36663  poimirlem32  37987  ftc1anc  38036  sdclem1  38078  sstotbnd2  38109  zerdivemp1x  38282  isdrngo2  38293  iscringd  38333  lsmsat  39468  lfladdcl  39531  lflnegcl  39535  lflvscl  39537  lshpkrlem4  39573  lshpkrlem6  39575  ldualgrplem  39605  lduallmodlem  39612  latmassOLD  39689  latm12  39690  latm32  39691  latmrot  39692  latmmdiN  39694  latmmdir  39695  omlfh1N  39718  omlfh3N  39719  cvlexchb1  39790  cvlexch3  39792  cvlexch4N  39793  cvlatexchb1  39794  cvlsupr2  39803  hlatjass  39830  hlatj12  39831  hlatj32  39832  cvratlem  39881  cvrat  39882  atcvrj0  39888  cvrat2  39889  atltcvr  39895  atexchltN  39901  cvrat3  39902  cvrat4  39903  3dimlem3  39921  3dimlem3OLDN  39922  3at  39950  2atneat  39975  llncmp  39982  2at0mat0  39985  2atmat0  39986  lplnnle2at  40001  llncvrlpln  40018  lplncmp  40022  lplnexllnN  40024  2llnjaN  40026  4atlem11  40069  lplncvrlvol  40076  lvolcmp  40077  2atm2atN  40245  elpaddatriN  40263  paddasslem9  40288  paddass  40298  padd12N  40299  paddssw2  40304  paddss  40305  pmodlem2  40307  pmodN  40310  pmapjlln1  40315  atmod1i1  40317  atmod1i2  40319  pexmidlem2N  40431  pexmidlem6N  40435  pl42N  40443  lhpm0atN  40489  lautlt  40551  lautcvr  40552  lautj  40553  lautm  40554  ltrneq2  40608  cdlemc3  40653  cdlemc4  40654  cdlemd1  40658  cdleme1b  40686  cdleme1  40687  cdleme2  40688  cdleme3e  40692  cdlemefr27cl  40863  cdlemefs27cl  40873  cdleme42mN  40947  cdlemftr2  41026  trljco  41200  tgrpgrplem  41209  tendoplass  41243  tendodi1  41244  tendodi2  41245  cdlemk36  41373  erngdvlem3  41450  erngdvlem3-rN  41458  tendospdi1  41480  dvalveclem  41485  dialss  41506  dvhvaddass  41557  dvhopvsca  41562  dvhlveclem  41568  diblss  41630  diclss  41653  dihmeetlem12N  41778  dihmeetlem15N  41781  dihmeetlem16N  41782  dihmeetlem17N  41783  dihmeetlem18N  41784  dihmeetlem19N  41785  dvh4dimN  41907  lpolvN  41946  lclkr  41993  lclkrs  41999  lcfr  42045  aks6d1c1  42569  irrapxlem6  43273  jm2.26lem3  43447  dgrsub2  43581  mpaadgr  43600  mendring  43634  mendlmod  43635  mendassa  43636  nnoeomeqom  43758  omabs2  43778  relexpmulg  44155  iunrelexpmin2  44157  relexpxpmin  44162  neicvgel1  44564  fmuldfeq  46031  stoweidlem43  46489  stoweidlem52  46498  stoweidlem53  46499  stoweidlem56  46502  stoweidlem57  46503  issmfle  47191  issmfgt  47202  issmfge  47216  submodaddmod  47807  fmtnoprmfac1  48040  fmtnoprmfac2  48042  clnbgredg  48328  cycl3grtrilem  48434  grlimprclnbgr  48484  grlimprclnbgredg  48485  upgrwlkupwlk  48628  copissgrp  48656  cznrng  48749  funcringcsetcALTV2lem9  48786  funcringcsetclem9ALTV  48809  linccl  48902  lincext1  48942  lincext3  48944  lincresunit2  48966  line  49220  rrxline  49222  itsclc0yqsol  49252  resipos  49462  topdlat  49491  catprs  49498  endmndlem  49502  idmon  49507  idepi  49508  thincmon  49920  thincepi  49921  grptcmon  50080  grptcepi  50081