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  9077  frfi  9175  intrnfi  9306  iinfi  9307  eqsup  9346  fisupcl  9360  cnfcomlem  9595  ttrclss  9616  ackbij1lem15  10130  fpwwe2lem4  10531  dedekindle  11283  ico0  13297  elioc2  13315  elico2  13316  elicc2  13317  iccsplit  13391  fseq1p1m1  13504  elfz0ubfz0  13538  hashtpg  14398  hash7g  14399  swrdsbslen  14578  ccatswrd  14582  wwlktovf1  14870  tanadd  16082  dvds2ln  16206  qredeq  16574  ressress  17164  mreexexlem4d  17559  mreexexd  17560  0catg  17600  2oppccomf  17637  issubc3  17762  fthmon  17842  fuccocl  17880  fucidcl  17881  invfuc  17890  initoeu2lem0  17926  initoeu2lem1  17927  curf2cl  18143  yonedalem4c  18189  yonedalem3  18192  pospo  18255  latjle12  18362  latjlej1  18365  latnlej2  18371  latlem12  18378  latmlem1  18381  latledi  18389  latmlej11  18390  latjass  18395  latj12  18396  latj32  18397  latj13  18398  latj31  18399  latjrot  18400  latjjdi  18403  latjjdir  18404  latdisdlem  18408  prdssgrpd  18647  prdsmndd  18684  imasmnd2  18688  mndissubm  18721  frmdmnd  18773  grpsubrcan  18940  grpsubadd  18947  grpsubsub  18948  grpaddsubass  18949  grpsubsub4  18952  grpnnncan2  18956  imasgrp2  18974  mulgnndir  19022  mulgnn0dir  19023  mulgdir  19025  mulgnnass  19028  mulgnn0ass  19029  mulgass  19030  mulgsubdir  19033  pwsmulg  19038  issubg2  19060  eqgval  19095  qusgrp  19104  kerf1ghm  19165  galcan  19222  gacan  19223  oppgmnd  19272  pmtrprfv  19371  pmtr3ncom  19393  psgnunilem3  19414  cmn32  19718  cmn12  19720  abladdsub  19730  ablsubaddsub  19732  mulgnn0di  19743  mulgdi  19744  mulgsubdi  19747  dprdss  19949  dprdz  19950  dprdf1o  19952  dprdsn  19956  dprd2da  19962  ablfac1b  19990  pgpfac1lem5  19999  prdsrngd  20100  imasrng  20101  srgbinomlem2  20151  srgbinom  20155  ringdilem  20173  prdsringd  20245  imasring  20254  opprrng  20269  mulgass3  20277  dvrass  20332  dvrdir  20336  subrgunit  20511  issubrg2  20513  abvdiv  20750  islss3  20898  prdslmodd  20908  islmhm2  20978  lspsolv  21086  islbs2  21097  islbs3  21098  lbsextlem4  21104  sralmod  21127  ipdir  21582  ipdi  21583  ipsubdir  21585  ipsubdi  21586  ipass  21588  ipassr  21589  ipassr2  21590  ocvlss  21615  sraassaOLD  21813  psrgrpOLD  21900  psrlmod  21903  psrring  21913  psrassa  21916  ply1ass23l  22145  mamudm  22316  matring  22364  matassa  22365  ofco2  22372  mdetunilem1  22533  mdetunilem9  22541  mdetuni0  22542  mdetmul  22544  gsummatr01lem3  22578  iinopn  22823  subbascn  23175  nrmsep2  23277  isnrm3  23280  regsep2  23297  dnsconst  23299  dfconn2  23340  1stcelcls  23382  nllyidm  23410  dislly  23418  upxp  23544  fbasne0  23751  filss  23774  infil  23784  fsubbas  23788  filssufilg  23832  tmdcn2  24010  psmettri  24232  isxmet2d  24248  xmettri  24272  xmetres2  24282  bldisj  24319  blss2ps  24324  blss2  24325  xmstri2  24387  mstri2  24388  xmstri  24389  mstri  24390  xmstri3  24391  mstri3  24392  msrtri  24393  comet  24434  stdbdbl  24438  met2ndci  24443  ngprcan  24531  ngplcan  24532  ngpsubcan  24535  nmtri2  24548  nrgdsdi  24586  nrgdsdir  24587  nlmdsdi  24602  nlmdsdir  24603  blcvx  24719  icccmplem2  24745  pi1grplem  24982  pi1cof  24992  clmpm1dir  25036  cvsdiv  25065  cvsdivcl  25066  cphdivcl  25115  cphsubdir  25141  cphsubdi  25142  cphassr  25145  bcthlem5  25261  rrxcph  25325  volfiniun  25481  volcn  25540  itg1val2  25618  dvconst  25851  dvlip  25931  dvfsumlem4  25969  ftc1a  25977  ulmval  26322  ulmdvlem3  26344  ang180  26757  cvxcl  26928  scvxcvx  26929  sgmmul  27145  logexprlim  27169  dchrabl  27198  nosupbnd1  27659  noinfbnd1lem5  27672  noinfbnd1  27674  ssltss1  27734  motgrp  28527  iscgra1  28794  cgrane1  28796  cgrane2  28797  cgrahl1  28800  cgrahl2  28801  cgracgr  28802  cgratr  28807  cgrabtwn  28810  dfcgra2  28814  sacgr  28815  f1otrge  28856  colinearalglem1  28891  colinearalg  28895  axcgrtr  28900  axlowdimlem16  28942  axeuclidlem  28947  axcontlem7  28955  eengtrkg  28971  eengtrkge  28972  nbfusgrlevtxm2  29363  lfgriswlk  29672  upgrwlkdvde  29722  wwlknbp1  29829  usgrwwlks2on  29943  erclwwlktr  30009  erclwwlkntr  30058  frgr2wwlkeqm  30318  numclwwlk1lem2f  30342  numclwwlk5  30375  friendship  30386  grpodivdiv  30527  grpomuldivass  30528  ablodivdiv4  30541  ablonnncan1  30544  nvmdi  30635  dipassr  30833  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  33613  ccfldsrarelvec  33691  constrconj  33765  constrfin  33766  constrelextdg2  33767  pstmfval  33916  tpr2rico  33932  qqhval2lem  34001  qqhvq  34007  issiga  34132  measdivcst  34244  measdivcstALTV  34245  carsggect  34338  signsply0  34571  tgoldbachgtd  34682  bnj149  34894  bnj1118  35003  bnj1128  35009  erdszelem9  35250  resconn  35297  cvmseu  35327  cvmlift2lem12  35365  ex-sategoelel  35472  elmrsubrn  35571  mclsind  35621  r1peuqusdeg1  35694  cgrid2  36054  segconeu  36062  btwncomim  36064  btwnswapid  36068  cgrxfr  36106  btwnxfr  36107  colineardim1  36112  brofs2  36128  brifs2  36129  idinside  36135  endofsegid  36136  btwnconn1lem7  36144  btwnconn1lem11  36148  btwnconn1  36152  segcon2  36156  seglemin  36164  segletr  36165  btwnsegle  36168  colinbtwnle  36169  broutsideof2  36173  broutsideof3  36177  outsidele  36183  fvray  36192  fvline  36195  linerflx1  36200  ellines  36203  ivthALT  36386  weiunpo  36516  poimirlem32  37698  ftc1anc  37747  sdclem1  37789  sstotbnd2  37820  zerdivemp1x  37993  isdrngo2  38004  iscringd  38044  lsmsat  39113  lfladdcl  39176  lflnegcl  39180  lflvscl  39182  lshpkrlem4  39218  lshpkrlem6  39220  ldualgrplem  39250  lduallmodlem  39257  latmassOLD  39334  latm12  39335  latm32  39336  latmrot  39337  latmmdiN  39339  latmmdir  39340  omlfh1N  39363  omlfh3N  39364  cvlexchb1  39435  cvlexch3  39437  cvlexch4N  39438  cvlatexchb1  39439  cvlsupr2  39448  hlatjass  39475  hlatj12  39476  hlatj32  39477  cvratlem  39526  cvrat  39527  atcvrj0  39533  cvrat2  39534  atltcvr  39540  atexchltN  39546  cvrat3  39547  cvrat4  39548  3dimlem3  39566  3dimlem3OLDN  39567  3at  39595  2atneat  39620  llncmp  39627  2at0mat0  39630  2atmat0  39631  lplnnle2at  39646  llncvrlpln  39663  lplncmp  39667  lplnexllnN  39669  2llnjaN  39671  4atlem11  39714  lplncvrlvol  39721  lvolcmp  39722  2atm2atN  39890  elpaddatriN  39908  paddasslem9  39933  paddass  39943  padd12N  39944  paddssw2  39949  paddss  39950  pmodlem2  39952  pmodN  39955  pmapjlln1  39960  atmod1i1  39962  atmod1i2  39964  pexmidlem2N  40076  pexmidlem6N  40080  pl42N  40088  lhpm0atN  40134  lautlt  40196  lautcvr  40197  lautj  40198  lautm  40199  ltrneq2  40253  cdlemc3  40298  cdlemc4  40299  cdlemd1  40303  cdleme1b  40331  cdleme1  40332  cdleme2  40333  cdleme3e  40337  cdlemefr27cl  40508  cdlemefs27cl  40518  cdleme42mN  40592  cdlemftr2  40671  trljco  40845  tgrpgrplem  40854  tendoplass  40888  tendodi1  40889  tendodi2  40890  cdlemk36  41018  erngdvlem3  41095  erngdvlem3-rN  41103  tendospdi1  41125  dvalveclem  41130  dialss  41151  dvhvaddass  41202  dvhopvsca  41207  dvhlveclem  41213  diblss  41275  diclss  41298  dihmeetlem12N  41423  dihmeetlem15N  41426  dihmeetlem16N  41427  dihmeetlem17N  41428  dihmeetlem18N  41429  dihmeetlem19N  41430  dvh4dimN  41552  lpolvN  41591  lclkr  41638  lclkrs  41644  lcfr  41690  aks6d1c1  42215  irrapxlem6  42925  jm2.26lem3  43099  dgrsub2  43233  mpaadgr  43252  mendring  43286  mendlmod  43287  mendassa  43288  nnoeomeqom  43410  omabs2  43430  relexpmulg  43808  iunrelexpmin2  43810  relexpxpmin  43815  neicvgel1  44217  fmuldfeq  45688  stoweidlem43  46146  stoweidlem52  46155  stoweidlem53  46156  stoweidlem56  46159  stoweidlem57  46160  issmfle  46848  issmfgt  46859  issmfge  46873  submodaddmod  47446  fmtnoprmfac1  47670  fmtnoprmfac2  47672  clnbgredg  47945  cycl3grtrilem  48051  grlimprclnbgr  48101  grlimprclnbgredg  48102  upgrwlkupwlk  48245  copissgrp  48273  cznrng  48366  funcringcsetcALTV2lem9  48403  funcringcsetclem9ALTV  48426  linccl  48520  lincext1  48560  lincext3  48562  lincresunit2  48584  line  48838  rrxline  48840  itsclc0yqsol  48870  resipos  49080  topdlat  49109  catprs  49117  endmndlem  49121  idmon  49126  idepi  49127  thincmon  49539  thincepi  49540  grptcmon  49699  grptcepi  49700