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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simpr12  1259  simpr22  1262  simpr32  1265  simp1r2  1271  simp2r2  1277  simp3r2  1283  3anandis  1472  fpr2g  7210  isopolem  7339  fr3nr  7756  sexp3  8136  dif1en  9157  frfi  9285  intrnfi  9408  fisupcl  9461  cnfcomlem  9691  ackbij1lem15  10226  cofsmo  10261  sornom  10269  fpwwe2lem4  10626  dedekindle  11375  supmul1  12180  eluzuzle  12828  xlesubadd  13239  elioc2  13384  elico2  13385  elicc2  13386  fseq1p1m1  13572  fz0fzelfz0  13604  swrdsbslen  14611  ccatswrd  14615  swrdswrdlem  14651  wwlktovf1  14905  tanadd  16107  dvds2ln  16229  cshwsidrepsw  17024  ressress  17190  f1ovscpbl  17469  mreexexlem4d  17588  mreexexd  17589  iscatd2  17622  2oppccomf  17668  issubc3  17796  fthmon  17875  fuccocl  17914  fucidcl  17915  invfuc  17924  initoeu2lem0  17960  initoeu2lem1  17961  curf2cl  18181  yonedalem4c  18227  yonedalem3  18230  pospo  18295  latjle12  18400  latjlej1  18403  latnlej2  18409  latlem12  18416  latmlem1  18419  latledi  18427  latjass  18433  latj12  18434  latj32  18435  latj13  18436  latj31  18437  latjrot  18438  latjjdi  18441  latjjdir  18442  latdisdlem  18446  prdssgrpd  18621  prdsmndd  18655  mndissubm  18685  frmdmnd  18737  grpsubrcan  18901  grpsubadd  18908  grpaddsubass  18910  grpsubsub4  18913  grppnpcan2  18914  grpnpncan  18915  mulgnndir  18978  mulgnn0dir  18979  mulgdir  18981  mulgnnass  18984  mulgnn0ass  18985  mulgass  18986  mulgsubdir  18989  pwsmulg  18994  issubg2  19016  eqgval  19052  qusgrp  19060  galcan  19163  gacan  19164  oppgmnd  19216  fvcosymgeq  19292  pmtrprfv  19316  psgnunilem3  19359  cmn32  19663  cmn12  19665  abladdsub  19675  ablsubaddsub  19677  ablsubsub23  19687  mulgdi  19689  mulgsubdi  19692  dprdss  19894  dprdz  19895  dprdf1o  19897  dprdsn  19901  dprd2da  19907  dmdprdsplit  19912  ablfac1b  19935  pgpfac1lem5  19944  srgdilem  20009  srgbinom  20048  ringdilem  20066  prdsringd  20128  opprring  20154  mulgass3  20160  dvrass  20215  dvrdir  20219  subrgunit  20374  issubrg2  20376  abvdiv  20438  lsssn0  20551  islss3  20563  prdslmodd  20573  islmhm2  20642  lspsolv  20749  islbs2  20760  islbs3  20761  lbsextlem4  20767  sralmod  20802  isdomn4  20911  psgndiflemB  21145  ipdir  21184  ipdi  21185  ipsubdir  21187  ipsubdi  21188  ipass  21190  ipassr  21191  ipassr2  21192  isphld  21199  ocvlss  21217  sraassab  21414  sraassaOLD  21416  psrbaglesuppOLD  21470  psrbagleclOLD  21472  psrbagconOLD  21476  psrgrpOLD  21510  psrlmod  21513  psrring  21523  psrassa  21526  mamudm  21882  matring  21937  matassa  21938  ofco2  21945  ma1repveval  22065  mdetunilem1  22106  mdetunilem9  22114  chpscmatgsumbin  22338  iinopn  22396  restopnb  22671  subbascn  22750  nrmsep2  22852  isnrm3  22855  regsep2  22872  dnsconst  22874  dfconn2  22915  1stcelcls  22957  dislly  22993  ptuni2  23072  tx1stc  23146  0nelfb  23327  infil  23359  fsubbas  23363  filssufilg  23407  hauspwpwf1  23483  cnextcn  23563  tmdcn2  23585  ustuqtoplem  23736  utopsnneiplem  23744  psmettri  23809  isxmet2d  23825  xmettri  23849  xmetres2  23859  bldisj  23896  blss2ps  23901  blss2  23902  xmstri2  23964  mstri2  23965  xmstri  23966  mstri  23967  xmstri3  23968  mstri3  23969  msrtri  23970  comet  24014  stdbdbl  24018  met2ndci  24023  ngprcan  24111  ngplcan  24112  ngpsubcan  24115  nmtri2  24128  nrgdsdi  24174  nrgdsdir  24175  nlmdsdi  24190  nlmdsdir  24191  blcvx  24306  icoopnst  24447  pi1grplem  24557  clmpm1dir  24611  cmodscmulexp  24630  cvsdiv  24640  cvsdivcl  24641  cphdivcl  24691  cphsubdir  24717  cphsubdi  24718  tcphcph  24746  bcthlem5  24837  volfiniun  25056  volcn  25115  itg1val2  25193  dvconst  25426  dvlip  25502  ftc1a  25546  ulmval  25884  ulmdvlem3  25906  ang180  26309  cvxcl  26479  scvxcvx  26480  sgmmul  26694  dchrabl  26747  gausslemma2dlem1a  26858  nosupbnd1  27207  noinfbnd1lem5  27220  noinfbnd1  27222  ssltss2  27281  addscom  27440  motgrp  27784  iscgra1  28051  cgrane1  28053  cgrane3  28055  cgrahl1  28057  cgrahl2  28058  cgracgr  28059  cgratr  28064  cgrabtwn  28067  cgrahl  28068  dfcgra2  28071  sacgr  28072  f1otrge  28113  colinearalglem1  28154  axcgrtr  28163  axeuclidlem  28210  axcontlem3  28214  axcontlem4  28215  axcontlem7  28218  eengtrkg  28234  eengtrkge  28235  edglnl  28393  subgruhgredgd  28531  nbfusgrlevtxm2  28625  lfgriswlk  28935  wwlknbp1  29088  umgrwwlks2on  29201  rusgrnumwwlks  29218  clwlkclwwlkfo  29252  3spthd  29419  3vfriswmgr  29521  frgr2wwlkeqm  29574  numclwwlk1lem2f  29598  numclwwlk2  29624  numclwwlk3  29628  numclwwlk5  29631  grpomuldivass  29782  ablomuldiv  29793  ablodivdiv4  29795  ablonnncan1  29798  nvmdi  29889  dipassr  30087  archiabllem2c  32329  dvrcan5  32374  reofld  32448  eqgvscpbl  32454  qusvsval  32456  quslmod  32458  quslmhm  32459  prmidlc  32556  ssmxidl  32579  ply1degltlss  32656  drgextlsp  32670  ccfldsrarelvec  32734  pstmfval  32865  qqhval2lem  32950  qqhvq  32956  measdivcst  33211  measdivcstALTV  33212  carsggect  33306  tgoldbachgtd  33663  bnj1098  33783  bnj149  33875  bnj1118  33984  erdszelem9  34179  resconn  34226  cvmseu  34256  cvmlift2lem10  34292  cvmlift2lem12  34294  ex-sategoelel  34401  elmrsubrn  34500  mclsind  34550  cgrid2  34964  segconeu  34972  btwncomim  34974  btwnswapid  34978  trisegint  34989  cgrxfr  35016  brofs2  35038  endofsegid  35046  btwnconn2  35063  seglemin  35074  segletr  35075  btwnsegle  35078  colinbtwnle  35079  broutsideof2  35083  btwnoutside  35086  broutsideof3  35087  outsideoftr  35090  outsidele  35093  fvray  35102  fvline  35105  ellines  35113  broucube  36511  ftc1anc  36558  sdclem1  36600  sstotbnd2  36631  iscringd  36855  lsmsat  37867  lfladdcl  37930  lflnegcl  37934  lflvscl  37936  eqlkr  37958  lshpkrlem4  37972  lshpkrlem6  37974  ldualgrplem  38004  lduallmodlem  38011  latmassOLD  38088  latm12  38089  latm32  38090  latmrot  38091  latmmdiN  38093  latmmdir  38094  omlfh1N  38117  omlfh3N  38118  cvrnbtwn2  38134  cvlexchb1  38189  cvlsupr2  38202  hlatjass  38229  hlatj12  38230  hlatj32  38231  cvrat  38282  cvrat2  38289  atltcvr  38295  atexchltN  38301  cvrat3  38302  cvrat4  38303  atbtwnexOLDN  38307  atbtwnex  38308  3dimlem3  38321  3dimlem3OLDN  38322  3at  38350  2atneat  38375  llncmp  38382  2at0mat0  38385  2atmat0  38386  llncvrlpln  38418  lplncmp  38422  2llnjaN  38426  4atlem11  38469  lplncvrlvol  38476  lvolcmp  38477  2atm2atN  38645  elpaddatriN  38663  paddasslem8  38687  paddass  38698  padd12N  38699  paddssw2  38704  paddss  38705  pmod1i  38708  pmodN  38710  pmapjlln1  38715  atmod1i1  38717  atmod1i2  38719  pexmidlem2N  38831  pl42lem2N  38840  pl42lem3N  38841  pl42lem4N  38842  pl42N  38843  lhpm0atN  38889  lautlt  38951  lautcvr  38952  lautj  38953  lautm  38954  ltrneq2  39008  cdlemd1  39058  cdleme1b  39086  cdleme1  39087  cdleme2  39088  cdleme3e  39092  cdlemefr27cl  39263  cdlemefs27cl  39273  cdleme42ke  39345  cdleme42mN  39347  cdlemf2  39422  cdlemftr2  39426  trljco  39600  tgrpgrplem  39609  tendoplass  39643  tendodi1  39644  tendodi2  39645  cdlemk34  39770  cdlemk36  39773  erngdvlem3-rN  39858  tendospdi1  39880  dialss  39906  dvhvaddass  39957  dvhopvsca  39962  dvhlveclem  39968  diblss  40030  diclss  40053  diclspsn  40054  cdlemn11pre  40070  dihmeetlem12N  40178  dihmeetlem16N  40182  dihmeetlem17N  40183  dihmeetlem18N  40184  dvh4dimN  40307  lpolconN  40347  dochpolN  40350  lclkr  40393  lclkrs  40399  lcfr  40445  irrapxlem6  41551  jm2.26lem3  41726  dgrsub2  41863  mpaaroot  41883  mendring  41920  mendlmod  41921  mendassa  41922  relexpmulg  42447  iunrelexpmin2  42449  relexpxpmin  42454  neicvgel1  42856  grumnud  43031  rfcnpre3  43703  fmuldfeq  44286  xlimbr  44530  stoweidlem43  44746  stoweidlem52  44755  stoweidlem53  44756  stoweidlem56  44759  stoweidlem57  44760  stoweidlem60  44763  issmfle  45448  issmfgt  45459  issmfge  45473  smflimlem4  45477  ltsubsubaddltsub  45996  iccpartigtl  46078  iccelpart  46088  prproropf1olem1  46158  fpprel2  46396  upgrwlkupwlk  46505  copissgrp  46565  opprrng  46661  prdsrngd  46664  rnglidl1  46736  cznrng  46807  funcringcsetcALTV2lem9  46896  funcringcsetclem9ALTV  46919  ldepsprlem  47107  lincresunit3  47116  lincreslvec3  47117  itsclc0yqe  47401  itsclc0yqsol  47404  topdlat  47583  catprs  47585  endmndlem  47589  idmon  47590  idepi  47591  thincmon  47608  thincepi  47609  functhinclem1  47615  grptcmon  47670  grptcepi  47671