Theorem simpr2 1191

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr12  1254  simpr22  1257  simpr32  1260  simp1r2  1266  simp2r2  1272  simp3r2  1278  3anandis  1467  fpr2g  6974  isopolem  7098  fr3nr  7494  frfi  8763  intrnfi  8880  fisupcl  8933  cnfcomlem  9162  ackbij1lem15  9656  cofsmo  9691  sornom  9699  fpwwe2lem5  10056  dedekindle  10804  supmul1  11610  eluzuzle  12253  xlesubadd  12657  elioc2  12800  elico2  12801  elicc2  12802  fseq1p1m1  12982  fz0fzelfz0  13014  swrdsbslen  14026  ccatswrd  14030  swrdswrdlem  14066  wwlktovf1  14321  tanadd  15520  dvds2ln  15642  cshwsidrepsw  16427  ressress  16562  f1ovscpbl  16799  mreexexlem4d  16918  mreexexd  16919  iscatd2  16952  2oppccomf  16995  issubc3  17119  fthmon  17197  fuccocl  17234  fucidcl  17235  invfuc  17244  initoeu2lem0  17273  initoeu2lem1  17274  curf2cl  17481  yonedalem4c  17527  yonedalem3  17530  pospo  17583  latjle12  17672  latjlej1  17675  latnlej2  17681  latlem12  17688  latmlem1  17691  latledi  17699  latjass  17705  latj12  17706  latj32  17707  latj13  17708  latj31  17709  latjrot  17710  latjjdi  17713  latjjdir  17714  latdisdlem  17799  prdsmndd  17944  mndissubm  17972  frmdmnd  18024  grpsubrcan  18180  grpsubadd  18187  grpaddsubass  18189  grpsubsub4  18192  grppnpcan2  18193  grpnpncan  18194  mulgnndir  18256  mulgnn0dir  18257  mulgdir  18259  mulgnnass  18262  mulgnn0ass  18263  mulgass  18264  mulgsubdir  18267  pwsmulg  18272  issubg2  18294  eqgval  18329  qusgrp  18335  galcan  18434  gacan  18435  oppgmnd  18482  fvcosymgeq  18557  pmtrprfv  18581  psgnunilem3  18624  cmn32  18925  cmn12  18927  abladdsub  18935  ablsubsub23  18945  mulgdi  18947  mulgsubdi  18950  dprdss  19151  dprdz  19152  dprdf1o  19154  dprdsn  19158  dprd2da  19164  dmdprdsplit  19169  ablfac1b  19192  pgpfac1lem5  19201  srgi  19261  srgbinom  19295  ringi  19310  prdsringd  19362  opprring  19381  mulgass3  19387  dvrass  19440  subrgunit  19553  issubrg2  19555  abvdiv  19608  lsssn0  19719  islss3  19731  prdslmodd  19741  islmhm2  19810  lspsolv  19915  islbs2  19926  islbs3  19927  lbsextlem4  19933  sralmod  19959  sraassa  20099  psrbaglesupp  20148  psrbaglecl  20149  psrbagcon  20151  psrgrp  20178  psrlmod  20181  psrring  20191  psrassa  20194  psgndiflemB  20744  ipdir  20783  ipdi  20784  ipsubdir  20786  ipsubdi  20787  ipass  20789  ipassr  20790  ipassr2  20791  isphld  20798  ocvlss  20816  mamudm  20999  matring  21052  matassa  21053  ofco2  21060  ma1repveval  21180  mdetunilem1  21221  mdetunilem9  21229  chpscmatgsumbin  21452  iinopn  21510  restopnb  21783  subbascn  21862  nrmsep2  21964  isnrm3  21967  regsep2  21984  dnsconst  21986  dfconn2  22027  1stcelcls  22069  dislly  22105  ptuni2  22184  tx1stc  22258  0nelfb  22439  infil  22471  fsubbas  22475  filssufilg  22519  hauspwpwf1  22595  cnextcn  22675  tmdcn2  22697  ustuqtoplem  22848  utopsnneiplem  22856  psmettri  22921  isxmet2d  22937  xmettri  22961  xmetres2  22971  bldisj  23008  blss2ps  23013  blss2  23014  xmstri2  23076  mstri2  23077  xmstri  23078  mstri  23079  xmstri3  23080  mstri3  23081  msrtri  23082  comet  23123  stdbdbl  23127  met2ndci  23132  ngprcan  23219  ngplcan  23220  ngpsubcan  23223  nmtri2  23236  nrgdsdi  23274  nrgdsdir  23275  nlmdsdi  23290  nlmdsdir  23291  blcvx  23406  icoopnst  23543  pi1grplem  23653  clmpm1dir  23707  cmodscmulexp  23726  cvsdiv  23736  cvsdivcl  23737  cphdivcl  23786  cphsubdir  23812  cphsubdi  23813  tcphcph  23840  bcthlem5  23931  volfiniun  24148  volcn  24207  itg1val2  24285  dvconst  24514  dvlip  24590  ftc1a  24634  ulmval  24968  ulmdvlem3  24990  ang180  25392  cvxcl  25562  scvxcvx  25563  sgmmul  25777  dchrabl  25830  gausslemma2dlem1a  25941  motgrp  26329  iscgra1  26596  cgrane1  26598  cgrane3  26600  cgrahl1  26602  cgrahl2  26603  cgracgr  26604  cgratr  26609  cgrabtwn  26612  cgrahl  26613  dfcgra2  26616  sacgr  26617  f1otrge  26658  colinearalglem1  26692  axcgrtr  26701  axeuclidlem  26748  axcontlem3  26752  axcontlem4  26753  axcontlem7  26756  eengtrkg  26772  eengtrkge  26773  edglnl  26928  subgruhgredgd  27066  nbfusgrlevtxm2  27160  lfgriswlk  27470  wwlknbp1  27622  umgrwwlks2on  27736  rusgrnumwwlks  27753  clwlkclwwlkfo  27787  3spthd  27955  3vfriswmgr  28057  frgr2wwlkeqm  28110  numclwwlk1lem2f  28134  numclwwlk2  28160  numclwwlk3  28164  numclwwlk5  28167  grpomuldivass  28318  ablomuldiv  28329  ablodivdiv4  28331  ablonnncan1  28334  nvmdi  28425  dipassr  28623  archiabllem2c  30824  dvrdir  30861  dvrcan5  30864  reofld  30913  eqgvscpbl  30919  qusscaval  30921  quslmod  30923  quslmhm  30924  prmidlc  30964  ssmxidl  30979  drgextlsp  30996  ccfldsrarelvec  31056  pstmfval  31136  qqhval2lem  31222  qqhvq  31228  measdivcst  31483  measdivcstALTV  31484  carsggect  31576  tgoldbachgtd  31933  bnj1098  32055  bnj149  32147  bnj1118  32256  erdszelem9  32446  resconn  32493  cvmseu  32523  cvmlift2lem10  32559  cvmlift2lem12  32561  ex-sategoelel  32668  elmrsubrn  32767  mclsind  32817  noprefixmo  33202  nosupbnd1  33214  ssltss2  33258  cgrid2  33464  segconeu  33472  btwncomim  33474  btwnswapid  33478  trisegint  33489  cgrxfr  33516  brofs2  33538  endofsegid  33546  btwnconn2  33563  seglemin  33574  segletr  33575  btwnsegle  33578  colinbtwnle  33579  broutsideof2  33583  btwnoutside  33586  broutsideof3  33587  outsideoftr  33590  outsidele  33593  fvray  33602  fvline  33605  ellines  33613  broucube  34941  ftc1anc  34990  sdclem1  35033  sstotbnd2  35067  iscringd  35291  lsmsat  36159  lfladdcl  36222  lflnegcl  36226  lflvscl  36228  eqlkr  36250  lshpkrlem4  36264  lshpkrlem6  36266  ldualgrplem  36296  lduallmodlem  36303  latmassOLD  36380  latm12  36381  latm32  36382  latmrot  36383  latmmdiN  36385  latmmdir  36386  omlfh1N  36409  omlfh3N  36410  cvrnbtwn2  36426  cvlexchb1  36481  cvlsupr2  36494  hlatjass  36521  hlatj12  36522  hlatj32  36523  cvrat  36573  cvrat2  36580  atltcvr  36586  atexchltN  36592  cvrat3  36593  cvrat4  36594  atbtwnexOLDN  36598  atbtwnex  36599  3dimlem3  36612  3dimlem3OLDN  36613  3at  36641  2atneat  36666  llncmp  36673  2at0mat0  36676  2atmat0  36677  llncvrlpln  36709  lplncmp  36713  2llnjaN  36717  4atlem11  36760  lplncvrlvol  36767  lvolcmp  36768  2atm2atN  36936  elpaddatriN  36954  paddasslem8  36978  paddass  36989  padd12N  36990  paddssw2  36995  paddss  36996  pmod1i  36999  pmodN  37001  pmapjlln1  37006  atmod1i1  37008  atmod1i2  37010  pexmidlem2N  37122  pl42lem2N  37131  pl42lem3N  37132  pl42lem4N  37133  pl42N  37134  lhpm0atN  37180  lautlt  37242  lautcvr  37243  lautj  37244  lautm  37245  ltrneq2  37299  cdlemd1  37349  cdleme1b  37377  cdleme1  37378  cdleme2  37379  cdleme3e  37383  cdlemefr27cl  37554  cdlemefs27cl  37564  cdleme42ke  37636  cdleme42mN  37638  cdlemf2  37713  cdlemftr2  37717  trljco  37891  tgrpgrplem  37900  tendoplass  37934  tendodi1  37935  tendodi2  37936  cdlemk34  38061  cdlemk36  38064  erngdvlem3-rN  38149  tendospdi1  38171  dialss  38197  dvhvaddass  38248  dvhopvsca  38253  dvhlveclem  38259  diblss  38321  diclss  38344  diclspsn  38345  cdlemn11pre  38361  dihmeetlem12N  38469  dihmeetlem16N  38473  dihmeetlem17N  38474  dihmeetlem18N  38475  dvh4dimN  38598  lpolconN  38638  dochpolN  38641  lclkr  38684  lclkrs  38690  lcfr  38736  irrapxlem6  39444  jm2.26lem3  39618  dgrsub2  39755  mpaaroot  39775  mendring  39812  mendlmod  39813  mendassa  39814  relexpmulg  40075  iunrelexpmin2  40077  relexpxpmin  40082  neicvgel1  40489  grumnud  40642  rfcnpre3  41310  fmuldfeq  41884  xlimbr  42128  stoweidlem43  42348  stoweidlem52  42357  stoweidlem53  42358  stoweidlem56  42361  stoweidlem57  42362  stoweidlem60  42365  issmfle  43042  issmfgt  43053  issmfge  43066  smflimlem4  43070  ltsubsubaddltsub  43521  iccpartigtl  43603  iccelpart  43613  prproropf1olem1  43685  fpprel2  43926  upgrwlkupwlk  44035  copissgrp  44095  cznrng  44246  funcringcsetcALTV2lem9  44335  funcringcsetclem9ALTV  44358  ldepsprlem  44547  lincresunit3  44556  lincreslvec3  44557  itsclc0yqe  44768  itsclc0yqsol  44771