Theorem simpr2 1192

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpr12  1255  simpr22  1258  simpr32  1261  simp1r2  1267  simp2r2  1273  simp3r2  1279  3anandis  1468  fpr2g  6951  isopolem  7077  fr3nr  7474  frfi  8747  intrnfi  8864  fisupcl  8917  cnfcomlem  9146  ackbij1lem15  9645  cofsmo  9680  sornom  9688  fpwwe2lem5  10045  dedekindle  10793  supmul1  11597  eluzuzle  12240  xlesubadd  12644  elioc2  12788  elico2  12789  elicc2  12790  fseq1p1m1  12976  fz0fzelfz0  13008  swrdsbslen  14017  ccatswrd  14021  swrdswrdlem  14057  wwlktovf1  14312  tanadd  15512  dvds2ln  15634  cshwsidrepsw  16419  ressress  16554  f1ovscpbl  16791  mreexexlem4d  16910  mreexexd  16911  iscatd2  16944  2oppccomf  16987  issubc3  17111  fthmon  17189  fuccocl  17226  fucidcl  17227  invfuc  17236  initoeu2lem0  17265  initoeu2lem1  17266  curf2cl  17473  yonedalem4c  17519  yonedalem3  17522  pospo  17575  latjle12  17664  latjlej1  17667  latnlej2  17673  latlem12  17680  latmlem1  17683  latledi  17691  latjass  17697  latj12  17698  latj32  17699  latj13  17700  latj31  17701  latjrot  17702  latjjdi  17705  latjjdir  17706  latdisdlem  17791  prdsmndd  17936  mndissubm  17964  frmdmnd  18016  grpsubrcan  18172  grpsubadd  18179  grpaddsubass  18181  grpsubsub4  18184  grppnpcan2  18185  grpnpncan  18186  mulgnndir  18248  mulgnn0dir  18249  mulgdir  18251  mulgnnass  18254  mulgnn0ass  18255  mulgass  18256  mulgsubdir  18259  pwsmulg  18264  issubg2  18286  eqgval  18321  qusgrp  18327  galcan  18426  gacan  18427  oppgmnd  18474  fvcosymgeq  18549  pmtrprfv  18573  psgnunilem3  18616  cmn32  18917  cmn12  18919  abladdsub  18928  ablsubsub23  18938  mulgdi  18940  mulgsubdi  18943  dprdss  19144  dprdz  19145  dprdf1o  19147  dprdsn  19151  dprd2da  19157  dmdprdsplit  19162  ablfac1b  19185  pgpfac1lem5  19194  srgi  19254  srgbinom  19288  ringi  19306  prdsringd  19358  opprring  19377  mulgass3  19383  dvrass  19436  subrgunit  19546  issubrg2  19548  abvdiv  19601  lsssn0  19712  islss3  19724  prdslmodd  19734  islmhm2  19803  lspsolv  19908  islbs2  19919  islbs3  19920  lbsextlem4  19926  sralmod  19952  psgndiflemB  20289  ipdir  20328  ipdi  20329  ipsubdir  20331  ipsubdi  20332  ipass  20334  ipassr  20335  ipassr2  20336  isphld  20343  ocvlss  20361  sraassa  20556  psrbaglesupp  20606  psrbaglecl  20607  psrbagcon  20609  psrgrp  20636  psrlmod  20639  psrring  20649  psrassa  20652  mamudm  20995  matring  21048  matassa  21049  ofco2  21056  ma1repveval  21176  mdetunilem1  21217  mdetunilem9  21225  chpscmatgsumbin  21449  iinopn  21507  restopnb  21780  subbascn  21859  nrmsep2  21961  isnrm3  21964  regsep2  21981  dnsconst  21983  dfconn2  22024  1stcelcls  22066  dislly  22102  ptuni2  22181  tx1stc  22255  0nelfb  22436  infil  22468  fsubbas  22472  filssufilg  22516  hauspwpwf1  22592  cnextcn  22672  tmdcn2  22694  ustuqtoplem  22845  utopsnneiplem  22853  psmettri  22918  isxmet2d  22934  xmettri  22958  xmetres2  22968  bldisj  23005  blss2ps  23010  blss2  23011  xmstri2  23073  mstri2  23074  xmstri  23075  mstri  23076  xmstri3  23077  mstri3  23078  msrtri  23079  comet  23120  stdbdbl  23124  met2ndci  23129  ngprcan  23216  ngplcan  23217  ngpsubcan  23220  nmtri2  23233  nrgdsdi  23271  nrgdsdir  23272  nlmdsdi  23287  nlmdsdir  23288  blcvx  23403  icoopnst  23544  pi1grplem  23654  clmpm1dir  23708  cmodscmulexp  23727  cvsdiv  23737  cvsdivcl  23738  cphdivcl  23787  cphsubdir  23813  cphsubdi  23814  tcphcph  23841  bcthlem5  23932  volfiniun  24151  volcn  24210  itg1val2  24288  dvconst  24520  dvlip  24596  ftc1a  24640  ulmval  24975  ulmdvlem3  24997  ang180  25400  cvxcl  25570  scvxcvx  25571  sgmmul  25785  dchrabl  25838  gausslemma2dlem1a  25949  motgrp  26337  iscgra1  26604  cgrane1  26606  cgrane3  26608  cgrahl1  26610  cgrahl2  26611  cgracgr  26612  cgratr  26617  cgrabtwn  26620  cgrahl  26621  dfcgra2  26624  sacgr  26625  f1otrge  26666  colinearalglem1  26700  axcgrtr  26709  axeuclidlem  26756  axcontlem3  26760  axcontlem4  26761  axcontlem7  26764  eengtrkg  26780  eengtrkge  26781  edglnl  26936  subgruhgredgd  27074  nbfusgrlevtxm2  27168  lfgriswlk  27478  wwlknbp1  27630  umgrwwlks2on  27743  rusgrnumwwlks  27760  clwlkclwwlkfo  27794  3spthd  27961  3vfriswmgr  28063  frgr2wwlkeqm  28116  numclwwlk1lem2f  28140  numclwwlk2  28166  numclwwlk3  28170  numclwwlk5  28173  grpomuldivass  28324  ablomuldiv  28335  ablodivdiv4  28337  ablonnncan1  28340  nvmdi  28431  dipassr  28629  archiabllem2c  30874  dvrdir  30912  dvrcan5  30915  reofld  30964  eqgvscpbl  30970  qusscaval  30972  quslmod  30974  quslmhm  30975  prmidlc  31032  ssmxidl  31050  drgextlsp  31084  ccfldsrarelvec  31144  pstmfval  31249  qqhval2lem  31332  qqhvq  31338  measdivcst  31593  measdivcstALTV  31594  carsggect  31686  tgoldbachgtd  32043  bnj1098  32165  bnj149  32257  bnj1118  32366  erdszelem9  32559  resconn  32606  cvmseu  32636  cvmlift2lem10  32672  cvmlift2lem12  32674  ex-sategoelel  32781  elmrsubrn  32880  mclsind  32930  noprefixmo  33315  nosupbnd1  33327  ssltss2  33371  cgrid2  33577  segconeu  33585  btwncomim  33587  btwnswapid  33591  trisegint  33602  cgrxfr  33629  brofs2  33651  endofsegid  33659  btwnconn2  33676  seglemin  33687  segletr  33688  btwnsegle  33691  colinbtwnle  33692  broutsideof2  33696  btwnoutside  33699  broutsideof3  33700  outsideoftr  33703  outsidele  33706  fvray  33715  fvline  33718  ellines  33726  broucube  35091  ftc1anc  35138  sdclem1  35181  sstotbnd2  35212  iscringd  35436  lsmsat  36304  lfladdcl  36367  lflnegcl  36371  lflvscl  36373  eqlkr  36395  lshpkrlem4  36409  lshpkrlem6  36411  ldualgrplem  36441  lduallmodlem  36448  latmassOLD  36525  latm12  36526  latm32  36527  latmrot  36528  latmmdiN  36530  latmmdir  36531  omlfh1N  36554  omlfh3N  36555  cvrnbtwn2  36571  cvlexchb1  36626  cvlsupr2  36639  hlatjass  36666  hlatj12  36667  hlatj32  36668  cvrat  36718  cvrat2  36725  atltcvr  36731  atexchltN  36737  cvrat3  36738  cvrat4  36739  atbtwnexOLDN  36743  atbtwnex  36744  3dimlem3  36757  3dimlem3OLDN  36758  3at  36786  2atneat  36811  llncmp  36818  2at0mat0  36821  2atmat0  36822  llncvrlpln  36854  lplncmp  36858  2llnjaN  36862  4atlem11  36905  lplncvrlvol  36912  lvolcmp  36913  2atm2atN  37081  elpaddatriN  37099  paddasslem8  37123  paddass  37134  padd12N  37135  paddssw2  37140  paddss  37141  pmod1i  37144  pmodN  37146  pmapjlln1  37151  atmod1i1  37153  atmod1i2  37155  pexmidlem2N  37267  pl42lem2N  37276  pl42lem3N  37277  pl42lem4N  37278  pl42N  37279  lhpm0atN  37325  lautlt  37387  lautcvr  37388  lautj  37389  lautm  37390  ltrneq2  37444  cdlemd1  37494  cdleme1b  37522  cdleme1  37523  cdleme2  37524  cdleme3e  37528  cdlemefr27cl  37699  cdlemefs27cl  37709  cdleme42ke  37781  cdleme42mN  37783  cdlemf2  37858  cdlemftr2  37862  trljco  38036  tgrpgrplem  38045  tendoplass  38079  tendodi1  38080  tendodi2  38081  cdlemk34  38206  cdlemk36  38209  erngdvlem3-rN  38294  tendospdi1  38316  dialss  38342  dvhvaddass  38393  dvhopvsca  38398  dvhlveclem  38404  diblss  38466  diclss  38489  diclspsn  38490  cdlemn11pre  38506  dihmeetlem12N  38614  dihmeetlem16N  38618  dihmeetlem17N  38619  dihmeetlem18N  38620  dvh4dimN  38743  lpolconN  38783  dochpolN  38786  lclkr  38829  lclkrs  38835  lcfr  38881  irrapxlem6  39768  jm2.26lem3  39942  dgrsub2  40079  mpaaroot  40099  mendring  40136  mendlmod  40137  mendassa  40138  relexpmulg  40411  iunrelexpmin2  40413  relexpxpmin  40418  neicvgel1  40822  grumnud  40994  rfcnpre3  41662  fmuldfeq  42225  xlimbr  42469  stoweidlem43  42685  stoweidlem52  42694  stoweidlem53  42695  stoweidlem56  42698  stoweidlem57  42699  stoweidlem60  42702  issmfle  43379  issmfgt  43390  issmfge  43403  smflimlem4  43407  ltsubsubaddltsub  43858  iccpartigtl  43940  iccelpart  43950  prproropf1olem1  44020  fpprel2  44259  upgrwlkupwlk  44368  copissgrp  44428  cznrng  44579  funcringcsetcALTV2lem9  44668  funcringcsetclem9ALTV  44691  ldepsprlem  44881  lincresunit3  44890  lincreslvec3  44891  itsclc0yqe  45175  itsclc0yqsol  45178