Theorem simpr2 1214

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr12  1277  simpr22  1280  simpr32  1283  simp1r2  1289  simp2r2  1295  simp3r2  1301  3anandis  1500  fpr2g  7216  isopolem  7354  fr3nr  7780  sexp3  8158  dif1en  9156  frfi  9255  intrnfi  9386  fisupcl  9440  cnfcomlem  9678  ackbij1lem15  10235  cofsmo  10271  sornom  10279  fpwwe2lem4  10637  dedekindle  11392  supmul1  12202  eluzuzle  12889  xlesubadd  13307  elioc2  13454  elico2  13455  elicc2  13456  fseq1p1m1  13645  fz0fzelfz0  13681  hash7g  14543  swrdsbslen  14726  ccatswrd  14730  swrdswrdlem  14765  wwlktovf1  15020  tanadd  16248  dvds2ln  16372  cshwsidrepsw  17178  ressress  17332  f1ovscpbl  17605  mreexexlem4d  17728  mreexexd  17729  iscatd2  17762  2oppccomf  17806  issubc3  17931  fthmon  18011  fuccocl  18049  fucidcl  18050  invfuc  18059  initoeu2lem0  18095  initoeu2lem1  18096  curf2cl  18312  yonedalem4c  18358  yonedalem3  18361  pospo  18424  latjle12  18531  latjlej1  18534  latnlej2  18540  latlem12  18547  latmlem1  18550  latledi  18558  latjass  18564  latj12  18565  latj32  18566  latj13  18567  latj31  18568  latjrot  18569  latjjdi  18572  latjjdir  18573  latdisdlem  18577  prdssgrpd  18816  prdsmndd  18853  mndissubm  18890  frmdmnd  18943  grpsubrcan  19112  grpsubadd  19119  grpaddsubass  19121  grpsubsub4  19124  grppnpcan2  19125  grpnpncan  19126  mulgnndir  19194  mulgnn0dir  19195  mulgdir  19197  mulgnnass  19200  mulgnn0ass  19201  mulgass  19202  mulgsubdir  19205  pwsmulg  19210  issubg2  19233  eqgval  19270  qusgrp  19282  galcan  19399  gacan  19400  oppgmnd  19449  fvcosymgeq  19524  pmtrprfv  19548  psgnunilem3  19591  cmn32  19895  cmn12  19897  abladdsub  19907  ablsubaddsub  19909  ablsubsub23  19919  mulgdi  19921  mulgsubdi  19924  dprdss  20126  dprdz  20127  dprdf1o  20129  dprdsn  20133  dprd2da  20139  dmdprdsplit  20144  ablfac1b  20167  pgpfac1lem5  20176  prdsrngd  20279  srgdilem  20299  srgbinom  20338  ringdilem  20356  prdsringd  20428  opprrng  20453  mulgass3  20461  dvrass  20516  dvrdir  20520  subrgunit  20719  issubrg2  20721  isdomn4  20844  abvdiv  20962  lsssn0  21099  islss3  21110  prdslmodd  21120  islmhm2  21189  lspsolv  21297  islbs2  21308  islbs3  21309  lbsextlem4  21315  sralmod  21338  rnglidl1  21388  prmidlc  21503  ssdifidl  21515  psgndiflemB  21780  ipdir  21819  ipdi  21820  ipsubdir  21822  ipsubdi  21823  ipass  21825  ipassr  21826  ipassr2  21827  isphld  21834  ocvlss  21852  sraassab  22048  psrlmod  22139  psrring  22149  psrassa  22152  mamudm  22582  matring  22630  matassa  22631  ofco2  22638  ma1repveval  22758  mdetunilem1  22799  mdetunilem9  22807  chpscmatgsumbin  23031  iinopn  23089  restopnb  23362  subbascn  23441  nrmsep2  23543  isnrm3  23546  regsep2  23563  dnsconst  23565  dfconn2  23606  1stcelcls  23648  dislly  23684  ptuni2  23763  tx1stc  23837  0nelfb  24018  infil  24050  fsubbas  24054  filssufilg  24098  hauspwpwf1  24174  cnextcn  24254  tmdcn2  24276  ustuqtoplem  24426  utopsnneiplem  24434  psmettri  24498  isxmet2d  24514  xmettri  24538  xmetres2  24548  bldisj  24585  blss2ps  24590  blss2  24591  xmstri2  24653  mstri2  24654  xmstri  24655  mstri  24656  xmstri3  24657  mstri3  24658  msrtri  24659  comet  24700  stdbdbl  24704  met2ndci  24709  ngprcan  24797  ngplcan  24798  ngpsubcan  24801  nmtri2  24814  nrgdsdi  24852  nrgdsdir  24853  nlmdsdi  24868  nlmdsdir  24869  blcvx  24985  icoopnst  25128  pi1grplem  25238  clmpm1dir  25292  cmodscmulexp  25311  cvsdiv  25321  cvsdivcl  25322  cphdivcl  25371  cphsubdir  25397  cphsubdi  25398  tcphcph  25426  bcthlem5  25517  volfiniun  25736  volcn  25795  itg1val2  25873  dvconst  26106  dvlip  26182  ftc1a  26226  ulmval  26573  ulmdvlem3  26595  ang180  27009  cvxcl  27179  scvxcvx  27180  sgmmul  27395  dchrabl  27448  gausslemma2dlem1a  27559  nosupbnd1  27908  noinfbnd1lem5  27921  noinfbnd1  27923  sltsss2  27989  addscom  28189  addbday  28241  motgrp  28842  iscgra1  29151  cgrane1  29153  cgrane3  29155  cgrahl1  29157  cgrahl2  29158  cgracgr  29159  cgratr  29164  cgrabtwn  29167  cgrahl  29168  dfcgra2  29171  sacgr  29172  f1otrge  29251  colinearalglem1  29286  axcgrtr  29295  axeuclidlem  29342  axcontlem3  29346  axcontlem4  29347  axcontlem7  29350  eengtrkg  29366  eengtrkge  29367  edglnl  29523  subgruhgredgd  29664  nbfusgrlevtxm2  29758  lfgriswlk  30066  wwlknbp1  30223  usgrwwlks2on  30337  umgrwwlks2on  30338  rusgrnumwwlks  30356  clwlkclwwlkfo  30390  3spthd  30557  3vfriswmgr  30659  frgr2wwlkeqm  30712  numclwwlk1lem2f  30736  numclwwlk2  30762  numclwwlk3  30766  numclwwlk5  30769  grpomuldivass  30923  ablomuldiv  30934  ablodivdiv4  30936  ablonnncan1  30939  nvmdi  31030  dipassr  31228  archiabllem2c  33539  dvrcan5  33579  rloccring  33615  reofld  33687  eqgvscpbl  33694  qusvsval  33696  quslmod  33702  quslmhm  33703  ssmxidl  33781  ply1degltlss  33910  r1plmhm  33923  drgextlsp  34008  ccfldsrarelvec  34085  constrconj  34159  constrfin  34160  constrelextdg2  34161  pstmfval  34310  qqhval2lem  34395  qqhvq  34401  measdivcst  34638  measdivcstALTV  34639  carsggect  34732  tgoldbachgtd  35073  bnj1098  35196  bnj149  35287  bnj1118  35396  erdszelem9  35704  resconn  35751  cvmseu  35781  cvmlift2lem10  35817  cvmlift2lem12  35819  ex-sategoelel  35926  elmrsubrn  36025  mclsind  36075  r1peuqusdeg1  36148  cgrid2  36508  segconeu  36516  btwncomim  36518  btwnswapid  36522  trisegint  36533  cgrxfr  36560  brofs2  36582  endofsegid  36590  btwnconn2  36607  seglemin  36618  segletr  36619  btwnsegle  36622  colinbtwnle  36623  broutsideof2  36627  btwnoutside  36630  broutsideof3  36631  outsideoftr  36634  outsidele  36637  fvray  36646  fvline  36649  ellines  36657  nmulprop  36695  weiunpo  37009  broucube  38338  ftc1anc  38385  sdclem1  38427  sstotbnd2  38458  iscringd  38682  lsmsat  39815  lfladdcl  39878  lflnegcl  39882  lflvscl  39884  eqlkr  39906  lshpkrlem4  39920  lshpkrlem6  39922  ldualgrplem  39952  lduallmodlem  39959  latmassOLD  40036  latm12  40037  latm32  40038  latmrot  40039  latmmdiN  40041  latmmdir  40042  omlfh1N  40065  omlfh3N  40066  cvrnbtwn2  40082  cvlexchb1  40137  cvlsupr2  40150  hlatjass  40177  hlatj12  40178  hlatj32  40179  cvrat  40229  cvrat2  40236  atltcvr  40242  atexchltN  40248  cvrat3  40249  cvrat4  40250  atbtwnexOLDN  40254  atbtwnex  40255  3dimlem3  40268  3dimlem3OLDN  40269  3at  40297  2atneat  40322  llncmp  40329  2at0mat0  40332  2atmat0  40333  llncvrlpln  40365  lplncmp  40369  2llnjaN  40373  4atlem11  40416  lplncvrlvol  40423  lvolcmp  40424  2atm2atN  40592  elpaddatriN  40610  paddasslem8  40634  paddass  40645  padd12N  40646  paddssw2  40651  paddss  40652  pmod1i  40655  pmodN  40657  pmapjlln1  40662  atmod1i1  40664  atmod1i2  40666  pexmidlem2N  40778  pl42lem2N  40787  pl42lem3N  40788  pl42lem4N  40789  pl42N  40790  lhpm0atN  40836  lautlt  40898  lautcvr  40899  lautj  40900  lautm  40901  ltrneq2  40955  cdlemd1  41005  cdleme1b  41033  cdleme1  41034  cdleme2  41035  cdleme3e  41039  cdlemefr27cl  41210  cdlemefs27cl  41220  cdleme42ke  41292  cdleme42mN  41294  cdlemf2  41369  cdlemftr2  41373  trljco  41547  tgrpgrplem  41556  tendoplass  41590  tendodi1  41591  tendodi2  41592  cdlemk34  41717  cdlemk36  41720  erngdvlem3-rN  41805  tendospdi1  41827  dialss  41853  dvhvaddass  41904  dvhopvsca  41909  dvhlveclem  41915  diblss  41977  diclss  42000  diclspsn  42001  cdlemn11pre  42017  dihmeetlem12N  42125  dihmeetlem16N  42129  dihmeetlem17N  42130  dihmeetlem18N  42131  dvh4dimN  42254  lpolconN  42294  dochpolN  42297  lclkr  42340  lclkrs  42346  lcfr  42392  aks6d1c1  42916  irrapxlem6  43587  jm2.26lem3  43761  dgrsub2  43895  mpaaroot  43915  mendring  43948  mendlmod  43949  mendassa  43950  relexpmulg  44469  iunrelexpmin2  44471  relexpxpmin  44476  neicvgel1  44878  grumnud  45029  rfcnpre3  45786  fmuldfeq  46332  xlimbr  46574  stoweidlem43  46790  stoweidlem52  46799  stoweidlem53  46800  stoweidlem56  46803  stoweidlem57  46804  stoweidlem60  46807  issmfle  47492  issmfgt  47503  issmfge  47517  smflimlem4  47521  ltsubsubaddltsub  48071  iccpartigtl  48205  iccelpart  48215  prproropf1olem1  48285  fpprel2  48539  cycl3grtrilem  48744  grlimprclnbgr  48794  upgrwlkupwlk  48938  copissgrp  48966  cznrng  49059  funcringcsetcALTV2lem9  49096  funcringcsetclem9ALTV  49119  idomcanl  49145  ldepsprlem  49285  lincresunit3  49294  lincreslvec3  49295  itsclc0yqe  49574  itsclc0yqsol  49577  resipos  49786  topdlat  49815  catprs  49822  endmndlem  49826  idmon  49831  idepi  49832  thincmon  50244  thincepi  50245  functhinclem1  50255  grptcmon  50404  grptcepi  50405