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  7214  isopolem  7350  fr3nr  7775  sexp3  8155  dif1en  9160  frfi  9259  intrnfi  9390  fisupcl  9444  cnfcomlem  9682  ackbij1lem15  10239  cofsmo  10275  sornom  10283  fpwwe2lem4  10647  dedekindle  11402  supmul1  12212  eluzuzle  12900  xlesubadd  13319  elioc2  13466  elico2  13467  elicc2  13468  fseq1p1m1  13657  fz0fzelfz0  13693  hash7g  14555  swrdsbslen  14738  ccatswrd  14742  swrdswrdlem  14777  wwlktovf1  15034  tanadd  16261  dvds2ln  16385  cshwsidrepsw  17191  ressress  17345  f1ovscpbl  17618  mreexexlem4d  17741  mreexexd  17742  iscatd2  17775  2oppccomf  17819  issubc3  17944  fthmon  18024  fuccocl  18062  fucidcl  18063  invfuc  18072  initoeu2lem0  18108  initoeu2lem1  18109  curf2cl  18325  yonedalem4c  18371  yonedalem3  18374  pospo  18437  latjle12  18544  latjlej1  18547  latnlej2  18553  latlem12  18560  latmlem1  18563  latledi  18571  latjass  18577  latj12  18578  latj32  18579  latj13  18580  latj31  18581  latjrot  18582  latjjdi  18585  latjjdir  18586  latdisdlem  18590  prdssgrpd  18841  prdsmndd  18883  mndissubm  18921  frmdmnd  18974  grpsubrcan  19150  grpsubadd  19157  grpaddsubass  19159  grpsubsub4  19162  grppnpcan2  19163  grpnpncan  19164  mulgnndir  19232  mulgnn0dir  19233  mulgdir  19235  mulgnnass  19238  mulgnn0ass  19239  mulgass  19240  mulgsubdir  19243  pwsmulg  19248  issubg2  19271  eqgval  19308  qusgrp  19320  galcan  19437  gacan  19438  oppgmnd  19487  fvcosymgeq  19562  pmtrprfv  19586  psgnunilem3  19629  cmn32  19933  cmn12  19935  abladdsub  19945  ablsubaddsub  19947  ablsubsub23  19957  mulgdi  19959  mulgsubdi  19962  dprdss  20164  dprdz  20165  dprdf1o  20167  dprdsn  20171  dprd2da  20177  dmdprdsplit  20182  ablfac1b  20205  pgpfac1lem5  20214  prdsrngd  20317  srgdilem  20337  srgbinom  20376  ringdilem  20394  prdsringd  20467  opprrng  20492  mulgass3  20500  dvrass  20555  dvrdir  20559  subrgunit  20758  issubrg2  20760  isdomn4  20883  abvdiv  21001  lsssn0  21138  islss3  21149  prdslmodd  21159  islmhm2  21228  lspsolv  21336  islbs2  21347  islbs3  21348  lbsextlem4  21354  sralmod  21377  rnglidl1  21427  prmidlc  21542  ssdifidl  21554  psgndiflemB  21819  ipdir  21858  ipdi  21859  ipsubdir  21861  ipsubdi  21862  ipass  21864  ipassr  21865  ipassr2  21866  isphld  21873  ocvlss  21891  sraassab  22089  psrlmod  22180  psrring  22190  psrassa  22193  mamudm  22623  matring  22671  matassa  22672  ofco2  22679  ma1repveval  22799  mdetunilem1  22840  mdetunilem9  22848  chpscmatgsumbin  23075  iinopn  23133  restopnb  23406  subbascn  23485  nrmsep2  23587  isnrm3  23590  regsep2  23607  dnsconst  23609  dfconn2  23650  1stcelcls  23693  dislly  23729  ptuni2  23808  tx1stc  23882  0nelfb  24063  infil  24095  fsubbas  24099  filssufilg  24143  hauspwpwf1  24219  cnextcn  24299  tmdcn2  24321  ustuqtoplem  24471  utopsnneiplem  24479  psmettri  24543  isxmet2d  24559  xmettri  24583  xmetres2  24593  bldisj  24630  blss2ps  24635  blss2  24636  xmstri2  24698  mstri2  24699  xmstri  24700  mstri  24701  xmstri3  24702  mstri3  24703  msrtri  24704  comet  24745  stdbdbl  24749  met2ndci  24754  ngprcan  24842  ngplcan  24843  ngpsubcan  24846  nmtri2  24859  nrgdsdi  24897  nrgdsdir  24898  nlmdsdi  24913  nlmdsdir  24914  blcvx  25030  icoopnst  25173  pi1grplem  25283  clmpm1dir  25337  cmodscmulexp  25356  cvsdiv  25366  cvsdivcl  25367  cphdivcl  25416  cphsubdir  25442  cphsubdi  25443  tcphcph  25471  bcthlem5  25562  volfiniun  25781  volcn  25840  itg1val2  25918  dvconst  26151  dvlip  26227  ftc1a  26271  ulmval  26623  ulmdvlem3  26645  ang180  27059  cvxcl  27229  scvxcvx  27230  sgmmul  27445  dchrabl  27498  gausslemma2dlem1a  27609  nosupbnd1  27958  noinfbnd1lem5  27971  noinfbnd1  27973  sltsss2  28039  addscom  28239  addbday  28291  motgrp  28893  iscgra1  29204  cgrane1  29206  cgrane3  29208  cgrahl1  29210  cgrahl2  29211  cgracgr  29212  cgratr  29217  cgrabtwn  29221  cgrahl  29222  dfcgra2  29225  sacgr  29226  angmgmaddcl  29278  f1otrge  29336  colinearalglem1  29371  axcgrtr  29380  axeuclidlem  29427  axcontlem3  29431  axcontlem4  29432  axcontlem7  29435  eengtrkg  29451  eengtrkge  29452  edglnl  29608  subgruhgredgd  29752  nbfusgrlevtxm2  29846  lfgriswlk  30158  wwlknbp1  30320  usgrwwlks2on  30434  umgrwwlks2on  30435  rusgrnumwwlks  30453  clwlkclwwlkfo  30487  3spthd  30664  3vfriswmgr  30766  frgr2wwlkeqm  30819  numclwwlk1lem2f  30843  numclwwlk2  30869  numclwwlk3  30873  numclwwlk5  30876  grpomuldivass  31030  ablomuldiv  31041  ablodivdiv4  31043  ablonnncan1  31046  nvmdi  31137  dipassr  31335  archiabllem2c  33643  dvrcan5  33683  rloccring  33719  reofld  33791  eqgvscpbl  33798  qusvsval  33800  quslmod  33806  quslmhm  33807  ssmxidl  33885  ply1degltlss  34014  r1plmhm  34027  drgextlsp  34112  ccfldsrarelvec  34189  constrconj  34263  constrfin  34264  constrelextdg2  34265  pstmfval  34414  qqhval2lem  34499  qqhvq  34505  measdivcst  34743  measdivcstALTV  34744  carsggect  34837  tgoldbachgtd  35178  bnj1098  35301  bnj149  35392  bnj1118  35501  erdszelem9  35786  resconn  35833  cvmseu  35863  cvmlift2lem10  35899  cvmlift2lem12  35901  ex-sategoelel  36008  elmrsubrn  36107  mclsind  36157  r1peuqusdeg1  36230  cgrid2  36591  segconeu  36599  btwncomim  36601  btwnswapid  36605  trisegint  36616  cgrxfr  36643  brofs2  36665  endofsegid  36673  btwnconn2  36690  seglemin  36701  segletr  36702  btwnsegle  36705  colinbtwnle  36706  broutsideof2  36710  btwnoutside  36713  broutsideof3  36714  outsideoftr  36717  outsidele  36720  fvray  36729  fvline  36732  ellines  36740  nmulprop  36778  weiunpo  37092  broucube  38411  ftc1anc  38458  sdclem1  38501  sstotbnd2  38532  iscringd  38756  lsmsat  39889  lfladdcl  39952  lflnegcl  39956  lflvscl  39958  eqlkr  39980  lshpkrlem4  39994  lshpkrlem6  39996  ldualgrplem  40026  lduallmodlem  40033  latmassOLD  40110  latm12  40111  latm32  40112  latmrot  40113  latmmdiN  40115  latmmdir  40116  omlfh1N  40139  omlfh3N  40140  cvrnbtwn2  40156  cvlexchb1  40211  cvlsupr2  40224  hlatjass  40251  hlatj12  40252  hlatj32  40253  cvrat  40303  cvrat2  40310  atltcvr  40316  atexchltN  40322  cvrat3  40323  cvrat4  40324  atbtwnexOLDN  40328  atbtwnex  40329  3dimlem3  40342  3dimlem3OLDN  40343  3at  40371  2atneat  40396  llncmp  40403  2at0mat0  40406  2atmat0  40407  llncvrlpln  40439  lplncmp  40443  2llnjaN  40447  4atlem11  40490  lplncvrlvol  40497  lvolcmp  40498  2atm2atN  40666  elpaddatriN  40684  paddasslem8  40708  paddass  40719  padd12N  40720  paddssw2  40725  paddss  40726  pmod1i  40729  pmodN  40731  pmapjlln1  40736  atmod1i1  40738  atmod1i2  40740  pexmidlem2N  40852  pl42lem2N  40861  pl42lem3N  40862  pl42lem4N  40863  pl42N  40864  lhpm0atN  40910  lautlt  40972  lautcvr  40973  lautj  40974  lautm  40975  ltrneq2  41029  cdlemd1  41079  cdleme1b  41107  cdleme1  41108  cdleme2  41109  cdleme3e  41113  cdlemefr27cl  41284  cdlemefs27cl  41294  cdleme42ke  41366  cdleme42mN  41368  cdlemf2  41443  cdlemftr2  41447  trljco  41621  tgrpgrplem  41630  tendoplass  41664  tendodi1  41665  tendodi2  41666  cdlemk34  41791  cdlemk36  41794  erngdvlem3-rN  41879  tendospdi1  41901  dialss  41927  dvhvaddass  41978  dvhopvsca  41983  dvhlveclem  41989  diblss  42051  diclss  42074  diclspsn  42075  cdlemn11pre  42091  dihmeetlem12N  42199  dihmeetlem16N  42203  dihmeetlem17N  42204  dihmeetlem18N  42205  dvh4dimN  42328  lpolconN  42368  dochpolN  42371  lclkr  42414  lclkrs  42420  lcfr  42466  aks6d1c1  42990  irrapxlem6  43676  jm2.26lem3  43850  dgrsub2  43984  mpaaroot  44004  mendring  44037  mendlmod  44038  mendassa  44039  relexpmulg  44558  iunrelexpmin2  44560  relexpxpmin  44565  neicvgel1  44967  grumnud  45118  rfcnpre3  45875  fmuldfeq  46421  xlimbr  46663  stoweidlem43  46879  stoweidlem52  46888  stoweidlem53  46889  stoweidlem56  46892  stoweidlem57  46893  stoweidlem60  46896  issmfle  47581  issmfgt  47592  issmfge  47606  smflimlem4  47610  tmachlem-franscan  47785  ltsubsubaddltsub  48197  iccpartigtl  48331  iccelpart  48341  prproropf1olem1  48411  fpprel2  48665  cycl3grtrilem  48870  grlimprclnbgr  48920  upgrwlkupwlk  49064  copissgrp  49091  cznrng  49184  funcringcsetcALTV2lem9  49221  funcringcsetclem9ALTV  49244  idomcanl  49270  ldepsprlem  49410  lincresunit3  49419  lincreslvec3  49420  itsclc0yqe  49699  itsclc0yqsol  49702  resipos  49909  topdlat  49938  catprs  49945  endmndlem  49949  idmon  49954  idepi  49955  thincmon  50367  thincepi  50368  functhinclem1  50378  grptcmon  50527  grptcepi  50528  nellindf  50811