Theorem simpr2 1196

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜒)
2	1	3ad2antr2 1190	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:  simpr12  1259  simpr22  1262  simpr32  1265  simp1r2  1271  simp2r2  1277  simp3r2  1283  3anandis  1473  fpr2g  7151  isopolem  7286  fr3nr  7712  sexp3  8093  dif1en  9084  frfi  9190  intrnfi  9325  fisupcl  9379  cnfcomlem  9614  ackbij1lem15  10146  cofsmo  10182  sornom  10190  fpwwe2lem4  10547  dedekindle  11298  supmul1  12112  eluzuzle  12762  xlesubadd  13183  elioc2  13330  elico2  13331  elicc2  13332  fseq1p1m1  13519  fz0fzelfz0  13555  hash7g  14411  swrdsbslen  14589  ccatswrd  14593  swrdswrdlem  14628  wwlktovf1  14882  tanadd  16094  dvds2ln  16218  cshwsidrepsw  17023  ressress  17176  f1ovscpbl  17448  mreexexlem4d  17571  mreexexd  17572  iscatd2  17605  2oppccomf  17649  issubc3  17774  fthmon  17854  fuccocl  17892  fucidcl  17893  invfuc  17902  initoeu2lem0  17938  initoeu2lem1  17939  curf2cl  18155  yonedalem4c  18201  yonedalem3  18204  pospo  18267  latjle12  18374  latjlej1  18377  latnlej2  18383  latlem12  18390  latmlem1  18393  latledi  18401  latjass  18407  latj12  18408  latj32  18409  latj13  18410  latj31  18411  latjrot  18412  latjjdi  18415  latjjdir  18416  latdisdlem  18420  prdssgrpd  18625  prdsmndd  18662  mndissubm  18699  frmdmnd  18751  grpsubrcan  18918  grpsubadd  18925  grpaddsubass  18927  grpsubsub4  18930  grppnpcan2  18931  grpnpncan  18932  mulgnndir  19000  mulgnn0dir  19001  mulgdir  19003  mulgnnass  19006  mulgnn0ass  19007  mulgass  19008  mulgsubdir  19011  pwsmulg  19016  issubg2  19038  eqgval  19074  qusgrp  19083  galcan  19201  gacan  19202  oppgmnd  19251  fvcosymgeq  19326  pmtrprfv  19350  psgnunilem3  19393  cmn32  19697  cmn12  19699  abladdsub  19709  ablsubaddsub  19711  ablsubsub23  19721  mulgdi  19723  mulgsubdi  19726  dprdss  19928  dprdz  19929  dprdf1o  19931  dprdsn  19935  dprd2da  19941  dmdprdsplit  19946  ablfac1b  19969  pgpfac1lem5  19978  prdsrngd  20079  srgdilem  20095  srgbinom  20134  ringdilem  20152  prdsringd  20224  opprrng  20248  mulgass3  20256  dvrass  20311  dvrdir  20315  subrgunit  20493  issubrg2  20495  isdomn4  20619  abvdiv  20732  lsssn0  20869  islss3  20880  prdslmodd  20890  islmhm2  20960  lspsolv  21068  islbs2  21079  islbs3  21080  lbsextlem4  21086  sralmod  21109  rnglidl1  21157  psgndiflemB  21525  ipdir  21564  ipdi  21565  ipsubdir  21567  ipsubdi  21568  ipass  21570  ipassr  21571  ipassr2  21572  isphld  21579  ocvlss  21597  sraassab  21793  sraassaOLD  21795  psrgrpOLD  21882  psrlmod  21885  psrring  21895  psrassa  21898  mamudm  22298  matring  22346  matassa  22347  ofco2  22354  ma1repveval  22474  mdetunilem1  22515  mdetunilem9  22523  chpscmatgsumbin  22747  iinopn  22805  restopnb  23078  subbascn  23157  nrmsep2  23259  isnrm3  23262  regsep2  23279  dnsconst  23281  dfconn2  23322  1stcelcls  23364  dislly  23400  ptuni2  23479  tx1stc  23553  0nelfb  23734  infil  23766  fsubbas  23770  filssufilg  23814  hauspwpwf1  23890  cnextcn  23970  tmdcn2  23992  ustuqtoplem  24143  utopsnneiplem  24151  psmettri  24215  isxmet2d  24231  xmettri  24255  xmetres2  24265  bldisj  24302  blss2ps  24307  blss2  24308  xmstri2  24370  mstri2  24371  xmstri  24372  mstri  24373  xmstri3  24374  mstri3  24375  msrtri  24376  comet  24417  stdbdbl  24421  met2ndci  24426  ngprcan  24514  ngplcan  24515  ngpsubcan  24518  nmtri2  24531  nrgdsdi  24569  nrgdsdir  24570  nlmdsdi  24585  nlmdsdir  24586  blcvx  24702  icoopnst  24852  pi1grplem  24965  clmpm1dir  25019  cmodscmulexp  25038  cvsdiv  25048  cvsdivcl  25049  cphdivcl  25098  cphsubdir  25124  cphsubdi  25125  tcphcph  25153  bcthlem5  25244  volfiniun  25464  volcn  25523  itg1val2  25601  dvconst  25834  dvlip  25914  ftc1a  25960  ulmval  26305  ulmdvlem3  26327  ang180  26740  cvxcl  26911  scvxcvx  26912  sgmmul  27128  dchrabl  27181  gausslemma2dlem1a  27292  nosupbnd1  27642  noinfbnd1lem5  27655  noinfbnd1  27657  ssltss2  27718  addscom  27896  addsbday  27947  motgrp  28506  iscgra1  28773  cgrane1  28775  cgrane3  28777  cgrahl1  28779  cgrahl2  28780  cgracgr  28781  cgratr  28786  cgrabtwn  28789  cgrahl  28790  dfcgra2  28793  sacgr  28794  f1otrge  28835  colinearalglem1  28869  axcgrtr  28878  axeuclidlem  28925  axcontlem3  28929  axcontlem4  28930  axcontlem7  28933  eengtrkg  28949  eengtrkge  28950  edglnl  29106  subgruhgredgd  29247  nbfusgrlevtxm2  29341  lfgriswlk  29650  wwlknbp1  29807  umgrwwlks2on  29920  rusgrnumwwlks  29937  clwlkclwwlkfo  29971  3spthd  30138  3vfriswmgr  30240  frgr2wwlkeqm  30293  numclwwlk1lem2f  30317  numclwwlk2  30343  numclwwlk3  30347  numclwwlk5  30350  grpomuldivass  30503  ablomuldiv  30514  ablodivdiv4  30516  ablonnncan1  30519  nvmdi  30610  dipassr  30808  archiabllem2c  33147  dvrcan5  33186  rloccring  33220  reofld  33291  eqgvscpbl  33297  qusvsval  33299  quslmod  33305  quslmhm  33306  prmidlc  33395  ssdifidl  33404  ssmxidl  33421  ply1degltlss  33538  r1plmhm  33551  drgextlsp  33565  ccfldsrarelvec  33642  constrconj  33711  constrfin  33712  constrelextdg2  33713  pstmfval  33862  qqhval2lem  33947  qqhvq  33953  measdivcst  34190  measdivcstALTV  34191  carsggect  34285  tgoldbachgtd  34629  bnj1098  34749  bnj149  34841  bnj1118  34950  erdszelem9  35171  resconn  35218  cvmseu  35248  cvmlift2lem10  35284  cvmlift2lem12  35286  ex-sategoelel  35393  elmrsubrn  35492  mclsind  35542  r1peuqusdeg1  35615  cgrid2  35976  segconeu  35984  btwncomim  35986  btwnswapid  35990  trisegint  36001  cgrxfr  36028  brofs2  36050  endofsegid  36058  btwnconn2  36075  seglemin  36086  segletr  36087  btwnsegle  36090  colinbtwnle  36091  broutsideof2  36095  btwnoutside  36098  broutsideof3  36099  outsideoftr  36102  outsidele  36105  fvray  36114  fvline  36117  ellines  36125  weiunpo  36438  broucube  37633  ftc1anc  37680  sdclem1  37722  sstotbnd2  37753  iscringd  37977  lsmsat  38986  lfladdcl  39049  lflnegcl  39053  lflvscl  39055  eqlkr  39077  lshpkrlem4  39091  lshpkrlem6  39093  ldualgrplem  39123  lduallmodlem  39130  latmassOLD  39207  latm12  39208  latm32  39209  latmrot  39210  latmmdiN  39212  latmmdir  39213  omlfh1N  39236  omlfh3N  39237  cvrnbtwn2  39253  cvlexchb1  39308  cvlsupr2  39321  hlatjass  39348  hlatj12  39349  hlatj32  39350  cvrat  39401  cvrat2  39408  atltcvr  39414  atexchltN  39420  cvrat3  39421  cvrat4  39422  atbtwnexOLDN  39426  atbtwnex  39427  3dimlem3  39440  3dimlem3OLDN  39441  3at  39469  2atneat  39494  llncmp  39501  2at0mat0  39504  2atmat0  39505  llncvrlpln  39537  lplncmp  39541  2llnjaN  39545  4atlem11  39588  lplncvrlvol  39595  lvolcmp  39596  2atm2atN  39764  elpaddatriN  39782  paddasslem8  39806  paddass  39817  padd12N  39818  paddssw2  39823  paddss  39824  pmod1i  39827  pmodN  39829  pmapjlln1  39834  atmod1i1  39836  atmod1i2  39838  pexmidlem2N  39950  pl42lem2N  39959  pl42lem3N  39960  pl42lem4N  39961  pl42N  39962  lhpm0atN  40008  lautlt  40070  lautcvr  40071  lautj  40072  lautm  40073  ltrneq2  40127  cdlemd1  40177  cdleme1b  40205  cdleme1  40206  cdleme2  40207  cdleme3e  40211  cdlemefr27cl  40382  cdlemefs27cl  40392  cdleme42ke  40464  cdleme42mN  40466  cdlemf2  40541  cdlemftr2  40545  trljco  40719  tgrpgrplem  40728  tendoplass  40762  tendodi1  40763  tendodi2  40764  cdlemk34  40889  cdlemk36  40892  erngdvlem3-rN  40977  tendospdi1  40999  dialss  41025  dvhvaddass  41076  dvhopvsca  41081  dvhlveclem  41087  diblss  41149  diclss  41172  diclspsn  41173  cdlemn11pre  41189  dihmeetlem12N  41297  dihmeetlem16N  41301  dihmeetlem17N  41302  dihmeetlem18N  41303  dvh4dimN  41426  lpolconN  41466  dochpolN  41469  lclkr  41512  lclkrs  41518  lcfr  41564  aks6d1c1  42089  irrapxlem6  42800  jm2.26lem3  42974  dgrsub2  43108  mpaaroot  43128  mendring  43161  mendlmod  43162  mendassa  43163  relexpmulg  43683  iunrelexpmin2  43685  relexpxpmin  43690  neicvgel1  44092  grumnud  44259  rfcnpre3  45011  fmuldfeq  45565  xlimbr  45809  stoweidlem43  46025  stoweidlem52  46034  stoweidlem53  46035  stoweidlem56  46038  stoweidlem57  46039  stoweidlem60  46042  issmfle  46727  issmfgt  46738  issmfge  46752  smflimlem4  46756  ltsubsubaddltsub  47286  iccpartigtl  47408  iccelpart  47418  prproropf1olem1  47488  fpprel2  47726  cycl3grtrilem  47929  grlimgrtrilem1  47977  upgrwlkupwlk  48112  copissgrp  48140  cznrng  48233  funcringcsetcALTV2lem9  48270  funcringcsetclem9ALTV  48293  ldepsprlem  48445  lincresunit3  48454  lincreslvec3  48455  itsclc0yqe  48734  itsclc0yqsol  48737  resipos  48947  topdlat  48976  catprs  48984  endmndlem  48988  idmon  48993  idepi  48994  thincmon  49406  thincepi  49407  functhinclem1  49417  grptcmon  49566  grptcepi  49567