Theorem simpr2 1202

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpr12  1265  simpr22  1268  simpr32  1271  simp1r2  1277  simp2r2  1283  simp3r2  1289  3anandis  1479  fpr2g  7162  isopolem  7296  fr3nr  7722  sexp3  8100  dif1en  9093  frfi  9192  intrnfi  9326  fisupcl  9380  cnfcomlem  9618  ackbij1lem15  10153  cofsmo  10189  sornom  10197  fpwwe2lem4  10555  dedekindle  11308  supmul1  12123  eluzuzle  12795  xlesubadd  13213  elioc2  13360  elico2  13361  elicc2  13362  fseq1p1m1  13550  fz0fzelfz0  13586  hash7g  14446  swrdsbslen  14625  ccatswrd  14629  swrdswrdlem  14664  wwlktovf1  14917  tanadd  16132  dvds2ln  16256  cshwsidrepsw  17062  ressress  17215  f1ovscpbl  17488  mreexexlem4d  17611  mreexexd  17612  iscatd2  17645  2oppccomf  17689  issubc3  17814  fthmon  17894  fuccocl  17932  fucidcl  17933  invfuc  17942  initoeu2lem0  17978  initoeu2lem1  17979  curf2cl  18195  yonedalem4c  18241  yonedalem3  18244  pospo  18307  latjle12  18414  latjlej1  18417  latnlej2  18423  latlem12  18430  latmlem1  18433  latledi  18441  latjass  18447  latj12  18448  latj32  18449  latj13  18450  latj31  18451  latjrot  18452  latjjdi  18455  latjjdir  18456  latdisdlem  18460  prdssgrpd  18699  prdsmndd  18736  mndissubm  18773  frmdmnd  18825  grpsubrcan  18995  grpsubadd  19002  grpaddsubass  19004  grpsubsub4  19007  grppnpcan2  19008  grpnpncan  19009  mulgnndir  19077  mulgnn0dir  19078  mulgdir  19080  mulgnnass  19083  mulgnn0ass  19084  mulgass  19085  mulgsubdir  19088  pwsmulg  19093  issubg2  19115  eqgval  19150  qusgrp  19159  galcan  19277  gacan  19278  oppgmnd  19327  fvcosymgeq  19402  pmtrprfv  19426  psgnunilem3  19469  cmn32  19773  cmn12  19775  abladdsub  19785  ablsubaddsub  19787  ablsubsub23  19797  mulgdi  19799  mulgsubdi  19802  dprdss  20004  dprdz  20005  dprdf1o  20007  dprdsn  20011  dprd2da  20017  dmdprdsplit  20022  ablfac1b  20045  pgpfac1lem5  20054  prdsrngd  20155  srgdilem  20171  srgbinom  20210  ringdilem  20228  prdsringd  20298  opprrng  20323  mulgass3  20331  dvrass  20386  dvrdir  20390  subrgunit  20569  issubrg2  20571  isdomn4  20695  abvdiv  20808  lsssn0  20945  islss3  20956  prdslmodd  20966  islmhm2  21035  lspsolv  21143  islbs2  21154  islbs3  21155  lbsextlem4  21161  sralmod  21184  rnglidl1  21232  psgndiflemB  21582  ipdir  21621  ipdi  21622  ipsubdir  21624  ipsubdi  21625  ipass  21627  ipassr  21628  ipassr2  21629  isphld  21636  ocvlss  21654  sraassab  21850  psrlmod  21941  psrring  21951  psrassa  21954  mamudm  22385  matring  22433  matassa  22434  ofco2  22441  ma1repveval  22561  mdetunilem1  22602  mdetunilem9  22610  chpscmatgsumbin  22834  iinopn  22892  restopnb  23165  subbascn  23244  nrmsep2  23346  isnrm3  23349  regsep2  23366  dnsconst  23368  dfconn2  23409  1stcelcls  23451  dislly  23487  ptuni2  23566  tx1stc  23640  0nelfb  23821  infil  23853  fsubbas  23857  filssufilg  23901  hauspwpwf1  23977  cnextcn  24057  tmdcn2  24079  ustuqtoplem  24229  utopsnneiplem  24237  psmettri  24301  isxmet2d  24317  xmettri  24341  xmetres2  24351  bldisj  24388  blss2ps  24393  blss2  24394  xmstri2  24456  mstri2  24457  xmstri  24458  mstri  24459  xmstri3  24460  mstri3  24461  msrtri  24462  comet  24503  stdbdbl  24507  met2ndci  24512  ngprcan  24600  ngplcan  24601  ngpsubcan  24604  nmtri2  24617  nrgdsdi  24655  nrgdsdir  24656  nlmdsdi  24671  nlmdsdir  24672  blcvx  24788  icoopnst  24931  pi1grplem  25041  clmpm1dir  25095  cmodscmulexp  25114  cvsdiv  25124  cvsdivcl  25125  cphdivcl  25174  cphsubdir  25200  cphsubdi  25201  tcphcph  25229  bcthlem5  25320  volfiniun  25539  volcn  25598  itg1val2  25676  dvconst  25909  dvlip  25985  ftc1a  26029  ulmval  26370  ulmdvlem3  26392  ang180  26803  cvxcl  26973  scvxcvx  26974  sgmmul  27189  dchrabl  27242  gausslemma2dlem1a  27353  nosupbnd1  27703  noinfbnd1lem5  27716  noinfbnd1  27718  sltsss2  27783  addscom  27983  addbday  28035  motgrp  28636  iscgra1  28903  cgrane1  28905  cgrane3  28907  cgrahl1  28909  cgrahl2  28910  cgracgr  28911  cgratr  28916  cgrabtwn  28919  cgrahl  28920  dfcgra2  28923  sacgr  28924  f1otrge  28965  colinearalglem1  29000  axcgrtr  29009  axeuclidlem  29056  axcontlem3  29060  axcontlem4  29061  axcontlem7  29064  eengtrkg  29080  eengtrkge  29081  edglnl  29237  subgruhgredgd  29378  nbfusgrlevtxm2  29472  lfgriswlk  29780  wwlknbp1  29937  usgrwwlks2on  30051  umgrwwlks2on  30052  rusgrnumwwlks  30070  clwlkclwwlkfo  30104  3spthd  30271  3vfriswmgr  30373  frgr2wwlkeqm  30426  numclwwlk1lem2f  30450  numclwwlk2  30476  numclwwlk3  30480  numclwwlk5  30483  grpomuldivass  30637  ablomuldiv  30648  ablodivdiv4  30650  ablonnncan1  30653  nvmdi  30744  dipassr  30942  archiabllem2c  33283  dvrcan5  33324  rloccring  33358  reofld  33433  eqgvscpbl  33440  qusvsval  33442  quslmod  33448  quslmhm  33449  prmidlc  33538  ssdifidl  33547  ssmxidl  33564  ply1degltlss  33686  r1plmhm  33700  drgextlsp  33785  ccfldsrarelvec  33862  constrconj  33936  constrfin  33937  constrelextdg2  33938  pstmfval  34087  qqhval2lem  34172  qqhvq  34178  measdivcst  34415  measdivcstALTV  34416  carsggect  34509  tgoldbachgtd  34853  bnj1098  34973  bnj149  35064  bnj1118  35173  erdszelem9  35428  resconn  35475  cvmseu  35505  cvmlift2lem10  35541  cvmlift2lem12  35543  ex-sategoelel  35650  elmrsubrn  35749  mclsind  35799  r1peuqusdeg1  35872  cgrid2  36232  segconeu  36240  btwncomim  36242  btwnswapid  36246  trisegint  36257  cgrxfr  36284  brofs2  36306  endofsegid  36314  btwnconn2  36331  seglemin  36342  segletr  36343  btwnsegle  36346  colinbtwnle  36347  broutsideof2  36351  btwnoutside  36354  broutsideof3  36355  outsideoftr  36358  outsidele  36361  fvray  36370  fvline  36373  ellines  36381  weiunpo  36694  broucube  38022  ftc1anc  38069  sdclem1  38111  sstotbnd2  38142  iscringd  38366  lsmsat  39501  lfladdcl  39564  lflnegcl  39568  lflvscl  39570  eqlkr  39592  lshpkrlem4  39606  lshpkrlem6  39608  ldualgrplem  39638  lduallmodlem  39645  latmassOLD  39722  latm12  39723  latm32  39724  latmrot  39725  latmmdiN  39727  latmmdir  39728  omlfh1N  39751  omlfh3N  39752  cvrnbtwn2  39768  cvlexchb1  39823  cvlsupr2  39836  hlatjass  39863  hlatj12  39864  hlatj32  39865  cvrat  39915  cvrat2  39922  atltcvr  39928  atexchltN  39934  cvrat3  39935  cvrat4  39936  atbtwnexOLDN  39940  atbtwnex  39941  3dimlem3  39954  3dimlem3OLDN  39955  3at  39983  2atneat  40008  llncmp  40015  2at0mat0  40018  2atmat0  40019  llncvrlpln  40051  lplncmp  40055  2llnjaN  40059  4atlem11  40102  lplncvrlvol  40109  lvolcmp  40110  2atm2atN  40278  elpaddatriN  40296  paddasslem8  40320  paddass  40331  padd12N  40332  paddssw2  40337  paddss  40338  pmod1i  40341  pmodN  40343  pmapjlln1  40348  atmod1i1  40350  atmod1i2  40352  pexmidlem2N  40464  pl42lem2N  40473  pl42lem3N  40474  pl42lem4N  40475  pl42N  40476  lhpm0atN  40522  lautlt  40584  lautcvr  40585  lautj  40586  lautm  40587  ltrneq2  40641  cdlemd1  40691  cdleme1b  40719  cdleme1  40720  cdleme2  40721  cdleme3e  40725  cdlemefr27cl  40896  cdlemefs27cl  40906  cdleme42ke  40978  cdleme42mN  40980  cdlemf2  41055  cdlemftr2  41059  trljco  41233  tgrpgrplem  41242  tendoplass  41276  tendodi1  41277  tendodi2  41278  cdlemk34  41403  cdlemk36  41406  erngdvlem3-rN  41491  tendospdi1  41513  dialss  41539  dvhvaddass  41590  dvhopvsca  41595  dvhlveclem  41601  diblss  41663  diclss  41686  diclspsn  41687  cdlemn11pre  41703  dihmeetlem12N  41811  dihmeetlem16N  41815  dihmeetlem17N  41816  dihmeetlem18N  41817  dvh4dimN  41940  lpolconN  41980  dochpolN  41983  lclkr  42026  lclkrs  42032  lcfr  42078  aks6d1c1  42602  irrapxlem6  43273  jm2.26lem3  43447  dgrsub2  43581  mpaaroot  43601  mendring  43634  mendlmod  43635  mendassa  43636  relexpmulg  44155  iunrelexpmin2  44157  relexpxpmin  44162  neicvgel1  44564  grumnud  44731  rfcnpre3  45482  fmuldfeq  46029  xlimbr  46271  stoweidlem43  46487  stoweidlem52  46496  stoweidlem53  46497  stoweidlem56  46500  stoweidlem57  46501  stoweidlem60  46504  issmfle  47189  issmfgt  47200  issmfge  47214  smflimlem4  47218  ltsubsubaddltsub  47765  iccpartigtl  47899  iccelpart  47909  prproropf1olem1  47979  fpprel2  48233  cycl3grtrilem  48438  grlimprclnbgr  48488  upgrwlkupwlk  48632  copissgrp  48660  cznrng  48753  funcringcsetcALTV2lem9  48790  funcringcsetclem9ALTV  48813  ldepsprlem  48964  lincresunit3  48973  lincreslvec3  48974  itsclc0yqe  49253  itsclc0yqsol  49256  resipos  49466  topdlat  49495  catprs  49502  endmndlem  49506  idmon  49511  idepi  49512  thincmon  49924  thincepi  49925  functhinclem1  49935  grptcmon  50084  grptcepi  50085