Theorem simpr2 1194

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 1188	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  1257  simpr22  1260  simpr32  1263  simp1r2  1269  simp2r2  1275  simp3r2  1281  3anandis  1470  fpr2g  7231  isopolem  7365  fr3nr  7791  sexp3  8177  dif1en  9199  frfi  9319  intrnfi  9454  fisupcl  9507  cnfcomlem  9737  ackbij1lem15  10271  cofsmo  10307  sornom  10315  fpwwe2lem4  10672  dedekindle  11423  supmul1  12235  eluzuzle  12885  xlesubadd  13302  elioc2  13447  elico2  13448  elicc2  13449  fseq1p1m1  13635  fz0fzelfz0  13671  hash7g  14522  swrdsbslen  14699  ccatswrd  14703  swrdswrdlem  14739  wwlktovf1  14993  tanadd  16200  dvds2ln  16323  cshwsidrepsw  17128  ressress  17294  f1ovscpbl  17573  mreexexlem4d  17692  mreexexd  17693  iscatd2  17726  2oppccomf  17772  issubc3  17900  fthmon  17981  fuccocl  18021  fucidcl  18022  invfuc  18031  initoeu2lem0  18067  initoeu2lem1  18068  curf2cl  18288  yonedalem4c  18334  yonedalem3  18337  pospo  18403  latjle12  18508  latjlej1  18511  latnlej2  18517  latlem12  18524  latmlem1  18527  latledi  18535  latjass  18541  latj12  18542  latj32  18543  latj13  18544  latj31  18545  latjrot  18546  latjjdi  18549  latjjdir  18550  latdisdlem  18554  prdssgrpd  18759  prdsmndd  18796  mndissubm  18833  frmdmnd  18885  grpsubrcan  19052  grpsubadd  19059  grpaddsubass  19061  grpsubsub4  19064  grppnpcan2  19065  grpnpncan  19066  mulgnndir  19134  mulgnn0dir  19135  mulgdir  19137  mulgnnass  19140  mulgnn0ass  19141  mulgass  19142  mulgsubdir  19145  pwsmulg  19150  issubg2  19172  eqgval  19208  qusgrp  19217  galcan  19335  gacan  19336  oppgmnd  19388  fvcosymgeq  19462  pmtrprfv  19486  psgnunilem3  19529  cmn32  19833  cmn12  19835  abladdsub  19845  ablsubaddsub  19847  ablsubsub23  19857  mulgdi  19859  mulgsubdi  19862  dprdss  20064  dprdz  20065  dprdf1o  20067  dprdsn  20071  dprd2da  20077  dmdprdsplit  20082  ablfac1b  20105  pgpfac1lem5  20114  prdsrngd  20194  srgdilem  20210  srgbinom  20249  ringdilem  20267  prdsringd  20335  opprrng  20362  mulgass3  20370  dvrass  20425  dvrdir  20429  subrgunit  20607  issubrg2  20609  isdomn4  20733  abvdiv  20847  lsssn0  20964  islss3  20975  prdslmodd  20985  islmhm2  21055  lspsolv  21163  islbs2  21174  islbs3  21175  lbsextlem4  21181  sralmod  21212  rnglidl1  21260  psgndiflemB  21636  ipdir  21675  ipdi  21676  ipsubdir  21678  ipsubdi  21679  ipass  21681  ipassr  21682  ipassr2  21683  isphld  21690  ocvlss  21708  sraassab  21906  sraassaOLD  21908  psrgrpOLD  21995  psrlmod  21998  psrring  22008  psrassa  22011  mamudm  22415  matring  22465  matassa  22466  ofco2  22473  ma1repveval  22593  mdetunilem1  22634  mdetunilem9  22642  chpscmatgsumbin  22866  iinopn  22924  restopnb  23199  subbascn  23278  nrmsep2  23380  isnrm3  23383  regsep2  23400  dnsconst  23402  dfconn2  23443  1stcelcls  23485  dislly  23521  ptuni2  23600  tx1stc  23674  0nelfb  23855  infil  23887  fsubbas  23891  filssufilg  23935  hauspwpwf1  24011  cnextcn  24091  tmdcn2  24113  ustuqtoplem  24264  utopsnneiplem  24272  psmettri  24337  isxmet2d  24353  xmettri  24377  xmetres2  24387  bldisj  24424  blss2ps  24429  blss2  24430  xmstri2  24492  mstri2  24493  xmstri  24494  mstri  24495  xmstri3  24496  mstri3  24497  msrtri  24498  comet  24542  stdbdbl  24546  met2ndci  24551  ngprcan  24639  ngplcan  24640  ngpsubcan  24643  nmtri2  24656  nrgdsdi  24702  nrgdsdir  24703  nlmdsdi  24718  nlmdsdir  24719  blcvx  24834  icoopnst  24983  pi1grplem  25096  clmpm1dir  25150  cmodscmulexp  25169  cvsdiv  25179  cvsdivcl  25180  cphdivcl  25230  cphsubdir  25256  cphsubdi  25257  tcphcph  25285  bcthlem5  25376  volfiniun  25596  volcn  25655  itg1val2  25733  dvconst  25967  dvlip  26047  ftc1a  26093  ulmval  26438  ulmdvlem3  26460  ang180  26872  cvxcl  27043  scvxcvx  27044  sgmmul  27260  dchrabl  27313  gausslemma2dlem1a  27424  nosupbnd1  27774  noinfbnd1lem5  27787  noinfbnd1  27789  ssltss2  27849  addscom  28014  addsbday  28065  motgrp  28566  iscgra1  28833  cgrane1  28835  cgrane3  28837  cgrahl1  28839  cgrahl2  28840  cgracgr  28841  cgratr  28846  cgrabtwn  28849  cgrahl  28850  dfcgra2  28853  sacgr  28854  f1otrge  28895  colinearalglem1  28936  axcgrtr  28945  axeuclidlem  28992  axcontlem3  28996  axcontlem4  28997  axcontlem7  29000  eengtrkg  29016  eengtrkge  29017  edglnl  29175  subgruhgredgd  29316  nbfusgrlevtxm2  29410  lfgriswlk  29721  wwlknbp1  29874  umgrwwlks2on  29987  rusgrnumwwlks  30004  clwlkclwwlkfo  30038  3spthd  30205  3vfriswmgr  30307  frgr2wwlkeqm  30360  numclwwlk1lem2f  30384  numclwwlk2  30410  numclwwlk3  30414  numclwwlk5  30417  grpomuldivass  30570  ablomuldiv  30581  ablodivdiv4  30583  ablonnncan1  30586  nvmdi  30677  dipassr  30875  archiabllem2c  33185  dvrcan5  33226  rloccring  33257  reofld  33352  eqgvscpbl  33358  qusvsval  33360  quslmod  33366  quslmhm  33367  prmidlc  33456  ssdifidl  33465  ssmxidl  33482  ply1degltlss  33597  r1plmhm  33610  drgextlsp  33623  ccfldsrarelvec  33696  constrconj  33750  constrfin  33751  constrelextdg2  33752  pstmfval  33857  qqhval2lem  33944  qqhvq  33950  measdivcst  34205  measdivcstALTV  34206  carsggect  34300  tgoldbachgtd  34656  bnj1098  34776  bnj149  34868  bnj1118  34977  erdszelem9  35184  resconn  35231  cvmseu  35261  cvmlift2lem10  35297  cvmlift2lem12  35299  ex-sategoelel  35406  elmrsubrn  35505  mclsind  35555  r1peuqusdeg1  35628  cgrid2  35985  segconeu  35993  btwncomim  35995  btwnswapid  35999  trisegint  36010  cgrxfr  36037  brofs2  36059  endofsegid  36067  btwnconn2  36084  seglemin  36095  segletr  36096  btwnsegle  36099  colinbtwnle  36100  broutsideof2  36104  btwnoutside  36107  broutsideof3  36108  outsideoftr  36111  outsidele  36114  fvray  36123  fvline  36126  ellines  36134  weiunpo  36448  broucube  37641  ftc1anc  37688  sdclem1  37730  sstotbnd2  37761  iscringd  37985  lsmsat  38990  lfladdcl  39053  lflnegcl  39057  lflvscl  39059  eqlkr  39081  lshpkrlem4  39095  lshpkrlem6  39097  ldualgrplem  39127  lduallmodlem  39134  latmassOLD  39211  latm12  39212  latm32  39213  latmrot  39214  latmmdiN  39216  latmmdir  39217  omlfh1N  39240  omlfh3N  39241  cvrnbtwn2  39257  cvlexchb1  39312  cvlsupr2  39325  hlatjass  39352  hlatj12  39353  hlatj32  39354  cvrat  39405  cvrat2  39412  atltcvr  39418  atexchltN  39424  cvrat3  39425  cvrat4  39426  atbtwnexOLDN  39430  atbtwnex  39431  3dimlem3  39444  3dimlem3OLDN  39445  3at  39473  2atneat  39498  llncmp  39505  2at0mat0  39508  2atmat0  39509  llncvrlpln  39541  lplncmp  39545  2llnjaN  39549  4atlem11  39592  lplncvrlvol  39599  lvolcmp  39600  2atm2atN  39768  elpaddatriN  39786  paddasslem8  39810  paddass  39821  padd12N  39822  paddssw2  39827  paddss  39828  pmod1i  39831  pmodN  39833  pmapjlln1  39838  atmod1i1  39840  atmod1i2  39842  pexmidlem2N  39954  pl42lem2N  39963  pl42lem3N  39964  pl42lem4N  39965  pl42N  39966  lhpm0atN  40012  lautlt  40074  lautcvr  40075  lautj  40076  lautm  40077  ltrneq2  40131  cdlemd1  40181  cdleme1b  40209  cdleme1  40210  cdleme2  40211  cdleme3e  40215  cdlemefr27cl  40386  cdlemefs27cl  40396  cdleme42ke  40468  cdleme42mN  40470  cdlemf2  40545  cdlemftr2  40549  trljco  40723  tgrpgrplem  40732  tendoplass  40766  tendodi1  40767  tendodi2  40768  cdlemk34  40893  cdlemk36  40896  erngdvlem3-rN  40981  tendospdi1  41003  dialss  41029  dvhvaddass  41080  dvhopvsca  41085  dvhlveclem  41091  diblss  41153  diclss  41176  diclspsn  41177  cdlemn11pre  41193  dihmeetlem12N  41301  dihmeetlem16N  41305  dihmeetlem17N  41306  dihmeetlem18N  41307  dvh4dimN  41430  lpolconN  41470  dochpolN  41473  lclkr  41516  lclkrs  41522  lcfr  41568  aks6d1c1  42098  irrapxlem6  42815  jm2.26lem3  42990  dgrsub2  43124  mpaaroot  43144  mendring  43177  mendlmod  43178  mendassa  43179  relexpmulg  43700  iunrelexpmin2  43702  relexpxpmin  43707  neicvgel1  44109  grumnud  44282  rfcnpre3  44971  fmuldfeq  45539  xlimbr  45783  stoweidlem43  45999  stoweidlem52  46008  stoweidlem53  46009  stoweidlem56  46012  stoweidlem57  46013  stoweidlem60  46016  issmfle  46701  issmfgt  46712  issmfge  46726  smflimlem4  46730  ltsubsubaddltsub  47251  iccpartigtl  47348  iccelpart  47358  prproropf1olem1  47428  fpprel2  47666  grlimgrtrilem1  47897  upgrwlkupwlk  47984  copissgrp  48012  cznrng  48105  funcringcsetcALTV2lem9  48142  funcringcsetclem9ALTV  48165  ldepsprlem  48318  lincresunit3  48327  lincreslvec3  48328  itsclc0yqe  48611  itsclc0yqsol  48614  topdlat  48793  catprs  48800  endmndlem  48804  idmon  48805  idepi  48806  thincmon  48834  thincepi  48835  functhinclem1  48841  grptcmon  48902  grptcepi  48903