Theorem simpr1 1193

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 485	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2antr1 1187	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpr11  1256  simpr21  1259  simpr31  1262  simp1r1  1268  simp2r1  1274  simp3r1  1280  3anandis  1470  fpr2g  7137  isopolem  7266  fr3nr  7676  suppfnss  8067  frrlem4  8167  frrlem8  8171  dif1en  9017  frfi  9145  intrnfi  9265  iinfi  9266  eqsup  9305  fisupcl  9318  cnfcomlem  9548  ttrclss  9569  ackbij1lem15  10083  fpwwe2lem4  10483  dedekindle  11232  ico0  13218  elioc2  13235  elico2  13236  elicc2  13237  iccsplit  13310  fseq1p1m1  13423  elfz0ubfz0  13453  hashtpg  14291  swrdsbslen  14467  ccatswrd  14471  wwlktovf1  14763  tanadd  15967  dvds2ln  16089  qredeq  16451  ressress  17047  mreexexlem4d  17445  mreexexd  17446  0catg  17486  2oppccomf  17525  issubc3  17653  fthmon  17732  fuccocl  17771  fucidcl  17772  invfuc  17781  initoeu2lem0  17817  initoeu2lem1  17818  curf2cl  18038  yonedalem4c  18084  yonedalem3  18087  pospo  18152  latjle12  18257  latjlej1  18260  latnlej2  18266  latlem12  18273  latmlem1  18276  latledi  18284  latmlej11  18285  latjass  18290  latj12  18291  latj32  18292  latj13  18293  latj31  18294  latjrot  18295  latjjdi  18298  latjjdir  18299  latdisdlem  18303  prdsmndd  18507  imasmnd2  18511  mndissubm  18535  frmdmnd  18586  grpsubrcan  18744  grpsubadd  18751  grpsubsub  18752  grpaddsubass  18753  grpsubsub4  18756  grpnnncan2  18760  imasgrp2  18778  mulgnndir  18820  mulgnn0dir  18821  mulgdir  18823  mulgnnass  18826  mulgnn0ass  18827  mulgass  18828  mulgsubdir  18831  pwsmulg  18836  issubg2  18858  eqgval  18893  qusgrp  18899  galcan  18998  gacan  18999  oppgmnd  19049  pmtrprfv  19149  pmtr3ncom  19171  psgnunilem3  19192  cmn32  19492  cmn12  19494  abladdsub  19503  mulgnn0di  19514  mulgdi  19515  mulgsubdi  19518  dprdss  19719  dprdz  19720  dprdf1o  19722  dprdsn  19726  dprd2da  19732  ablfac1b  19760  pgpfac1lem5  19769  srgbinomlem2  19864  srgbinom  19868  ringdilem  19886  prdsringd  19938  imasring  19945  opprring  19960  mulgass3  19966  dvrass  20019  kerf1ghm  20077  subrgunit  20139  issubrg2  20141  abvdiv  20195  islss3  20319  prdslmodd  20329  islmhm2  20398  lspsolv  20503  islbs2  20514  islbs3  20515  lbsextlem4  20521  sralmod  20555  ipdir  20942  ipdi  20943  ipsubdir  20945  ipsubdi  20946  ipass  20948  ipassr  20949  ipassr2  20950  ocvlss  20975  sraassa  21172  psrbagleclOLD  21228  psrbagconOLD  21232  psrgrp  21265  psrlmod  21268  psrring  21278  psrassa  21281  mamudm  21635  matring  21690  matassa  21691  ofco2  21698  mdetunilem1  21859  mdetunilem9  21867  mdetuni0  21868  mdetmul  21870  gsummatr01lem3  21904  iinopn  22149  subbascn  22503  nrmsep2  22605  isnrm3  22608  regsep2  22625  dnsconst  22627  dfconn2  22668  1stcelcls  22710  nllyidm  22738  dislly  22746  upxp  22872  fbasne0  23079  filss  23102  infil  23112  fsubbas  23116  filssufilg  23160  tmdcn2  23338  psmettri  23562  isxmet2d  23578  xmettri  23602  xmetres2  23612  bldisj  23649  blss2ps  23654  blss2  23655  xmstri2  23717  mstri2  23718  xmstri  23719  mstri  23720  xmstri3  23721  mstri3  23722  msrtri  23723  comet  23767  stdbdbl  23771  met2ndci  23776  ngprcan  23864  ngplcan  23865  ngpsubcan  23868  nmtri2  23881  nrgdsdi  23927  nrgdsdir  23928  nlmdsdi  23943  nlmdsdir  23944  blcvx  24059  icccmplem2  24084  pi1grplem  24310  pi1cof  24320  clmpm1dir  24364  cvsdiv  24393  cvsdivcl  24394  cphdivcl  24444  cphsubdir  24470  cphsubdi  24471  cphassr  24474  bcthlem5  24590  rrxcph  24654  volfiniun  24809  volcn  24868  itg1val2  24946  dvconst  25179  dvlip  25255  dvfsumlem4  25291  ftc1a  25299  ulmval  25637  ulmdvlem3  25659  ang180  26062  cvxcl  26232  scvxcvx  26233  sgmmul  26447  logexprlim  26471  dchrabl  26500  nosupbnd1  26960  noinfbnd1lem5  26973  noinfbnd1  26975  motgrp  27106  iscgra1  27373  cgrane1  27375  cgrane2  27376  cgrahl1  27379  cgrahl2  27380  cgracgr  27381  cgratr  27386  cgrabtwn  27389  dfcgra2  27393  sacgr  27394  f1otrge  27435  colinearalglem1  27476  colinearalg  27480  axcgrtr  27485  axlowdimlem16  27527  axeuclidlem  27532  axcontlem7  27540  eengtrkg  27556  eengtrkge  27557  nbfusgrlevtxm2  27947  lfgriswlk  28257  upgrwlkdvde  28306  wwlknbp1  28410  erclwwlktr  28587  erclwwlkntr  28636  frgr2wwlkeqm  28896  numclwwlk1lem2f  28920  numclwwlk5  28953  friendship  28964  grpodivdiv  29103  grpomuldivass  29104  ablodivdiv4  29117  ablonnncan1  29120  nvmdi  29211  dipassr  29409  archiabllem2c  31649  dvrdir  31687  dvrcan5  31690  reofld  31753  eqgvscpbl  31759  qusscaval  31761  quslmod  31763  quslmhm  31764  prmidlc  31834  ssmxidl  31852  drgextlsp  31892  ccfldsrarelvec  31952  pstmfval  32057  tpr2rico  32073  qqhval2lem  32142  qqhvq  32148  issiga  32291  measdivcst  32403  measdivcstALTV  32404  carsggect  32498  signsply0  32743  tgoldbachgtd  32855  bnj149  33067  bnj1118  33176  bnj1128  33182  erdszelem9  33373  resconn  33420  cvmseu  33450  cvmlift2lem12  33488  ex-sategoelel  33595  elmrsubrn  33694  mclsind  33744  xpord3pred  33996  sexp3  33997  ssltss1  34074  cgrid2  34396  segconeu  34404  btwncomim  34406  btwnswapid  34410  cgrxfr  34448  btwnxfr  34449  colineardim1  34454  brofs2  34470  brifs2  34471  idinside  34477  endofsegid  34478  btwnconn1lem7  34486  btwnconn1lem11  34490  btwnconn1  34494  segcon2  34498  seglemin  34506  segletr  34507  btwnsegle  34510  colinbtwnle  34511  broutsideof2  34515  broutsideof3  34519  outsidele  34525  fvray  34534  fvline  34537  linerflx1  34542  ellines  34545  ivthALT  34615  poimirlem32  35907  ftc1anc  35956  sdclem1  35999  sstotbnd2  36030  zerdivemp1x  36203  isdrngo2  36214  iscringd  36254  lsmsat  37268  lfladdcl  37331  lflnegcl  37335  lflvscl  37337  lshpkrlem4  37373  lshpkrlem6  37375  ldualgrplem  37405  lduallmodlem  37412  latmassOLD  37489  latm12  37490  latm32  37491  latmrot  37492  latmmdiN  37494  latmmdir  37495  omlfh1N  37518  omlfh3N  37519  cvlexchb1  37590  cvlexch3  37592  cvlexch4N  37593  cvlatexchb1  37594  cvlsupr2  37603  hlatjass  37630  hlatj12  37631  hlatj32  37632  cvratlem  37682  cvrat  37683  atcvrj0  37689  cvrat2  37690  atltcvr  37696  atexchltN  37702  cvrat3  37703  cvrat4  37704  3dimlem3  37722  3dimlem3OLDN  37723  3at  37751  2atneat  37776  llncmp  37783  2at0mat0  37786  2atmat0  37787  lplnnle2at  37802  llncvrlpln  37819  lplncmp  37823  lplnexllnN  37825  2llnjaN  37827  4atlem11  37870  lplncvrlvol  37877  lvolcmp  37878  2atm2atN  38046  elpaddatriN  38064  paddasslem9  38089  paddass  38099  padd12N  38100  paddssw2  38105  paddss  38106  pmodlem2  38108  pmodN  38111  pmapjlln1  38116  atmod1i1  38118  atmod1i2  38120  pexmidlem2N  38232  pexmidlem6N  38236  pl42N  38244  lhpm0atN  38290  lautlt  38352  lautcvr  38353  lautj  38354  lautm  38355  ltrneq2  38409  cdlemc3  38454  cdlemc4  38455  cdlemd1  38459  cdleme1b  38487  cdleme1  38488  cdleme2  38489  cdleme3e  38493  cdlemefr27cl  38664  cdlemefs27cl  38674  cdleme42mN  38748  cdlemftr2  38827  trljco  39001  tgrpgrplem  39010  tendoplass  39044  tendodi1  39045  tendodi2  39046  cdlemk36  39174  erngdvlem3  39251  erngdvlem3-rN  39259  tendospdi1  39281  dvalveclem  39286  dialss  39307  dvhvaddass  39358  dvhopvsca  39363  dvhlveclem  39369  diblss  39431  diclss  39454  dihmeetlem12N  39579  dihmeetlem15N  39582  dihmeetlem16N  39583  dihmeetlem17N  39584  dihmeetlem18N  39585  dihmeetlem19N  39586  dvh4dimN  39708  lpolvN  39747  lclkr  39794  lclkrs  39800  lcfr  39846  irrapxlem6  40899  jm2.26lem3  41074  dgrsub2  41211  mpaadgr  41230  mendring  41268  mendlmod  41269  mendassa  41270  omabs2  41305  relexpmulg  41628  iunrelexpmin2  41630  relexpxpmin  41635  neicvgel1  42039  fmuldfeq  43449  stoweidlem43  43909  stoweidlem52  43918  stoweidlem53  43919  stoweidlem56  43922  stoweidlem57  43923  issmfle  44609  issmfgt  44620  issmfge  44634  fmtnoprmfac1  45357  fmtnoprmfac2  45359  upgrwlkupwlk  45642  copissgrp  45702  cznrng  45853  funcringcsetcALTV2lem9  45942  funcringcsetclem9ALTV  45965  ply1ass23l  46063  linccl  46095  lincext1  46135  lincext3  46137  lincresunit2  46159  line  46418  rrxline  46420  itsclc0yqsol  46450  topdlat  46630  catprs  46632  endmndlem  46636  idmon  46637  idepi  46638  thincmon  46655  thincepi  46656  grptcmon  46717  grptcepi  46718