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  7217  isopolem  7353  fr3nr  7786  sexp3  8172  dif1en  9180  frfi  9279  intrnfi  9411  fisupcl  9465  cnfcomlem  9703  ackbij1lem15  10314  cofsmo  10350  sornom  10358  fpwwe2lem4  10722  dedekindle  11477  supmul1  12289  eluzuzle  12977  xlesubadd  13396  elioc2  13543  elico2  13544  elicc2  13545  fseq1p1m1  13735  fz0fzelfz0  13771  hash7g  14634  swrdsbslen  14818  ccatswrd  14822  swrdswrdlem  14857  wwlktovf1  15115  tanadd  16340  dvds2ln  16464  cshwsidrepsw  17276  ressress  17430  f1ovscpbl  17703  mreexexlem4d  17826  mreexexd  17827  iscatd2  17860  2oppccomf  17904  issubc3  18029  fthmon  18109  fuccocl  18147  fucidcl  18148  invfuc  18157  initoeu2lem0  18193  initoeu2lem1  18194  curf2cl  18410  yonedalem4c  18456  yonedalem3  18459  pospo  18522  latjle12  18629  latjlej1  18632  latnlej2  18638  latlem12  18645  latmlem1  18648  latledi  18656  latjass  18662  latj12  18663  latj32  18664  latj13  18665  latj31  18666  latjrot  18667  latjjdi  18670  latjjdir  18671  latdisdlem  18675  prdssgrpd  18927  prdsmndd  18969  mndissubm  19007  frmdmnd  19060  grpsubrcan  19236  grpsubadd  19243  grpaddsubass  19245  grpsubsub4  19248  grppnpcan2  19249  grpnpncan  19250  mulgnndir  19318  mulgnn0dir  19319  mulgdir  19321  mulgnnass  19324  mulgnn0ass  19325  mulgass  19326  mulgsubdir  19329  pwsmulg  19334  issubg2  19357  eqgval  19394  qusgrp  19406  galcan  19523  gacan  19524  oppgmnd  19573  fvcosymgeq  19648  pmtrprfv  19672  psgnunilem3  19715  cmn32  20019  cmn12  20021  abladdsub  20031  ablsubaddsub  20033  ablsubsub23  20043  mulgdi  20045  mulgsubdi  20048  dprdss  20250  dprdz  20251  dprdf1o  20253  dprdsn  20257  dprd2da  20263  dmdprdsplit  20268  ablfac1b  20291  pgpfac1lem5  20300  prdsrngd  20403  srgdilem  20423  srgbinom  20462  ringdilem  20481  prdsringd  20555  opprrng  20580  mulgass3  20588  dvrass  20643  dvrdir  20647  subrgunit  20847  issubrg2  20849  isdomn4  20972  abvdiv  21091  lsssn0  21228  islss3  21239  prdslmodd  21249  islmhm2  21318  lspsolv  21426  islbs2  21437  islbs3  21438  lbsextlem4  21444  sralmod  21467  rnglidl1  21517  prmidlc  21634  ssdifidl  21646  psgndiflemB  21911  ipdir  21950  ipdi  21951  ipsubdir  21953  ipsubdi  21954  ipass  21956  ipassr  21957  ipassr2  21958  isphld  21965  ocvlss  21983  sraassab  22181  psrlmod  22272  psrring  22282  psrassa  22285  mamudm  22715  matring  22763  matassa  22764  ofco2  22771  ma1repveval  22891  mdetunilem1  22932  mdetunilem9  22940  chpscmatgsumbin  23167  iinopn  23225  restopnb  23498  subbascn  23577  nrmsep2  23679  isnrm3  23682  regsep2  23699  dnsconst  23701  dfconn2  23742  1stcelcls  23785  dislly  23821  ptuni2  23900  tx1stc  23974  0nelfb  24155  infil  24187  fsubbas  24191  filssufilg  24235  hauspwpwf1  24311  cnextcn  24391  tmdcn2  24413  ustuqtoplem  24563  utopsnneiplem  24571  psmettri  24635  isxmet2d  24651  xmettri  24675  xmetres2  24685  bldisj  24722  blss2ps  24727  blss2  24728  xmstri2  24790  mstri2  24791  xmstri  24792  mstri  24793  xmstri3  24794  mstri3  24795  msrtri  24796  comet  24837  stdbdbl  24841  met2ndci  24846  ngprcan  24934  ngplcan  24935  ngpsubcan  24938  nmtri2  24951  nrgdsdi  24989  nrgdsdir  24990  nlmdsdi  25005  nlmdsdir  25006  blcvx  25122  icoopnst  25265  pi1grplem  25375  clmpm1dir  25429  cmodscmulexp  25448  cvsdiv  25458  cvsdivcl  25459  cphdivcl  25508  cphsubdir  25534  cphsubdi  25535  tcphcph  25563  bcthlem5  25654  volfiniun  25873  volcn  25932  itg1val2  26010  dvconst  26242  dvlip  26318  ftc1a  26362  ulmval  26712  ulmdvlem3  26734  ang180  27147  cvxcl  27317  scvxcvx  27318  sgmmul  27533  dchrabl  27586  gausslemma2dlem1a  27697  nosupbnd1  28076  noinfbnd1lem5  28089  noinfbnd1  28091  sltsss2  28157  addscom  28357  addbday  28409  motgrp  29011  iscgra1  29322  cgrane1  29324  cgrane3  29326  cgrahl1  29328  cgrahl2  29329  cgracgr  29330  cgratr  29335  cgrabtwn  29339  cgrahl  29340  dfcgra2  29343  sacgr  29344  angmgmaddcl  29396  f1otrge  29454  colinearalglem1  29489  axcgrtr  29498  axeuclidlem  29545  axcontlem3  29549  axcontlem4  29550  axcontlem7  29553  eengtrkg  29569  eengtrkge  29570  edglnl  29726  subgruhgredgd  29870  nbfusgrlevtxm2  29964  lfgriswlk  30276  wwlknbp1  30438  usgrwwlks2on  30552  umgrwwlks2on  30553  rusgrnumwwlks  30571  clwlkclwwlkfo  30605  3spthd  30782  3vfriswmgr  30884  frgr2wwlkeqm  30937  numclwwlk1lem2f  30961  numclwwlk2  30987  numclwwlk3  30991  numclwwlk5  30994  grpomuldivass  31148  ablomuldiv  31159  ablodivdiv4  31161  ablonnncan1  31164  nvmdi  31255  dipassr  31453  archiabllem2c  33802  dvrcan5  33842  rloccring  33878  reofld  33950  eqgvscpbl  33957  qusvsval  33959  quslmod  33965  quslmhm  33966  ssmxidl  34045  ply1degltlss  34174  r1plmhm  34187  drgextlsp  34272  ccfldsrarelvec  34349  constrconj  34423  constrfin  34424  constrelextdg2  34425  pstmfval  34574  qqhval2lem  34659  qqhvq  34665  measdivcst  34903  measdivcstALTV  34904  carsggect  34996  tgoldbachgtd  35337  bnj1098  35460  bnj149  35551  bnj1118  35660  erdszelem9  36050  resconn  36097  cvmseu  36127  cvmlift2lem10  36163  cvmlift2lem12  36165  ex-sategoelel  36272  elmrsubrn  36371  mclsind  36421  r1peuqusdeg1  36494  cgrid2  36860  segconeu  36868  btwncomim  36870  btwnswapid  36874  trisegint  36885  cgrxfr  36912  brofs2  36934  endofsegid  36942  btwnconn2  36959  seglemin  36970  segletr  36971  btwnsegle  36974  colinbtwnle  36975  broutsideof2  36979  btwnoutside  36982  broutsideof3  36983  outsideoftr  36986  outsidele  36989  fvray  36998  fvline  37001  ellines  37009  nmulprop  37031  weiunpo  37345  broucube  38665  ftc1anc  38712  sdclem1  38770  sstotbnd2  38801  iscringd  39025  lsmsat  40158  lfladdcl  40221  lflnegcl  40225  lflvscl  40227  eqlkr  40249  lshpkrlem4  40263  lshpkrlem6  40265  ldualgrplem  40295  lduallmodlem  40302  latmassOLD  40379  latm12  40380  latm32  40381  latmrot  40382  latmmdiN  40384  latmmdir  40385  omlfh1N  40408  omlfh3N  40409  cvrnbtwn2  40425  cvlexchb1  40480  cvlsupr2  40493  hlatjass  40520  hlatj12  40521  hlatj32  40522  cvrat  40572  cvrat2  40579  atltcvr  40585  atexchltN  40591  cvrat3  40592  cvrat4  40593  atbtwnexOLDN  40597  atbtwnex  40598  3dimlem3  40611  3dimlem3OLDN  40612  3at  40640  2atneat  40665  llncmp  40672  2at0mat0  40675  2atmat0  40676  llncvrlpln  40708  lplncmp  40712  2llnjaN  40716  4atlem11  40759  lplncvrlvol  40766  lvolcmp  40767  2atm2atN  40935  elpaddatriN  40953  paddasslem8  40977  paddass  40988  padd12N  40989  paddssw2  40994  paddss  40995  pmod1i  40998  pmodN  41000  pmapjlln1  41005  atmod1i1  41007  atmod1i2  41009  pexmidlem2N  41121  pl42lem2N  41130  pl42lem3N  41131  pl42lem4N  41132  pl42N  41133  lhpm0atN  41179  lautlt  41241  lautcvr  41242  lautj  41243  lautm  41244  ltrneq2  41298  cdlemd1  41348  cdleme1b  41376  cdleme1  41377  cdleme2  41378  cdleme3e  41382  cdlemefr27cl  41553  cdlemefs27cl  41563  cdleme42ke  41635  cdleme42mN  41637  cdlemf2  41712  cdlemftr2  41716  trljco  41890  tgrpgrplem  41899  tendoplass  41933  tendodi1  41934  tendodi2  41935  cdlemk34  42060  cdlemk36  42063  erngdvlem3-rN  42148  tendospdi1  42170  dialss  42196  dvhvaddass  42247  dvhopvsca  42252  dvhlveclem  42258  diblss  42320  diclss  42343  diclspsn  42344  cdlemn11pre  42360  dihmeetlem12N  42468  dihmeetlem16N  42472  dihmeetlem17N  42473  dihmeetlem18N  42474  dvh4dimN  42597  lpolconN  42637  dochpolN  42640  lclkr  42683  lclkrs  42689  lcfr  42735  aks6d1c1  43259  irrapxlem6  43927  jm2.26lem3  44101  dgrsub2  44230  mpaaroot  44250  mendring  44283  mendlmod  44284  mendassa  44285  relexpmulg  44803  iunrelexpmin2  44805  relexpxpmin  44810  neicvgel1  45212  grumnud  45363  rfcnpre3  46143  fmuldfeq  46688  xlimbr  46930  stoweidlem43  47146  stoweidlem52  47155  stoweidlem53  47156  stoweidlem56  47159  stoweidlem57  47160  stoweidlem60  47163  issmfle  47848  issmfgt  47859  issmfge  47873  smflimlem4  47877  tmachlem-franscan  48052  ltsubsubaddltsub  48464  iccpartigtl  48598  iccelpart  48608  prproropf1olem1  48678  fpprel2  48932  cycl3grtrilem  49137  grlimprclnbgr  49187  upgrwlkupwlk  49331  copissgrp  49358  cznrng  49451  funcringcsetcALTV2lem9  49488  funcringcsetclem9ALTV  49511  idomcanl  49537  ldepsprlem  49677  lincresunit3  49686  lincreslvec3  49687  itsclc0yqe  49966  itsclc0yqsol  49969  resipos  50182  topdlat  50211  catprs  50218  endmndlem  50222  idmon  50227  idepi  50228  thincmon  50661  thincepi  50662  functhinclem1  50672  grptcmon  50824  grptcepi  50825  nellindf  51138