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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 206  df-an 396  df-3an 1086

This theorem is referenced by:  simpr12  1255  simpr22  1258  simpr32  1261  simp1r2  1267  simp2r2  1273  simp3r2  1279  3anandis  1467  fpr2g  7204  isopolem  7334  fr3nr  7752  sexp3  8133  dif1en  9156  frfi  9284  intrnfi  9407  fisupcl  9460  cnfcomlem  9690  ackbij1lem15  10225  cofsmo  10260  sornom  10268  fpwwe2lem4  10625  dedekindle  11375  supmul1  12180  eluzuzle  12828  xlesubadd  13239  elioc2  13384  elico2  13385  elicc2  13386  fseq1p1m1  13572  fz0fzelfz0  13604  swrdsbslen  14611  ccatswrd  14615  swrdswrdlem  14651  wwlktovf1  14905  tanadd  16107  dvds2ln  16229  cshwsidrepsw  17026  ressress  17192  f1ovscpbl  17471  mreexexlem4d  17590  mreexexd  17591  iscatd2  17624  2oppccomf  17670  issubc3  17798  fthmon  17879  fuccocl  17919  fucidcl  17920  invfuc  17929  initoeu2lem0  17965  initoeu2lem1  17966  curf2cl  18186  yonedalem4c  18232  yonedalem3  18235  pospo  18300  latjle12  18405  latjlej1  18408  latnlej2  18414  latlem12  18421  latmlem1  18424  latledi  18432  latjass  18438  latj12  18439  latj32  18440  latj13  18441  latj31  18442  latjrot  18443  latjjdi  18446  latjjdir  18447  latdisdlem  18451  prdssgrpd  18656  prdsmndd  18690  mndissubm  18722  frmdmnd  18774  grpsubrcan  18939  grpsubadd  18946  grpaddsubass  18948  grpsubsub4  18951  grppnpcan2  18952  grpnpncan  18953  mulgnndir  19020  mulgnn0dir  19021  mulgdir  19023  mulgnnass  19026  mulgnn0ass  19027  mulgass  19028  mulgsubdir  19031  pwsmulg  19036  issubg2  19058  eqgval  19094  qusgrp  19102  galcan  19210  gacan  19211  oppgmnd  19263  fvcosymgeq  19339  pmtrprfv  19363  psgnunilem3  19406  cmn32  19710  cmn12  19712  abladdsub  19722  ablsubaddsub  19724  ablsubsub23  19734  mulgdi  19736  mulgsubdi  19739  dprdss  19941  dprdz  19942  dprdf1o  19944  dprdsn  19948  dprd2da  19954  dmdprdsplit  19959  ablfac1b  19982  pgpfac1lem5  19991  prdsrngd  20071  srgdilem  20087  srgbinom  20126  ringdilem  20144  prdsringd  20210  opprrng  20237  mulgass3  20245  dvrass  20300  dvrdir  20304  subrgunit  20482  issubrg2  20484  abvdiv  20670  lsssn0  20785  islss3  20796  prdslmodd  20806  islmhm2  20876  lspsolv  20984  islbs2  20995  islbs3  20996  lbsextlem4  21002  sralmod  21033  rnglidl1  21081  isdomn4  21202  psgndiflemB  21461  ipdir  21500  ipdi  21501  ipsubdir  21503  ipsubdi  21504  ipass  21506  ipassr  21507  ipassr2  21508  isphld  21515  ocvlss  21533  sraassab  21730  sraassaOLD  21732  psrbaglesuppOLD  21787  psrbagleclOLD  21789  psrbagconOLD  21793  psrgrpOLD  21828  psrlmod  21831  psrring  21841  psrassa  21844  mamudm  22212  matring  22267  matassa  22268  ofco2  22275  ma1repveval  22395  mdetunilem1  22436  mdetunilem9  22444  chpscmatgsumbin  22668  iinopn  22726  restopnb  23001  subbascn  23080  nrmsep2  23182  isnrm3  23185  regsep2  23202  dnsconst  23204  dfconn2  23245  1stcelcls  23287  dislly  23323  ptuni2  23402  tx1stc  23476  0nelfb  23657  infil  23689  fsubbas  23693  filssufilg  23737  hauspwpwf1  23813  cnextcn  23893  tmdcn2  23915  ustuqtoplem  24066  utopsnneiplem  24074  psmettri  24139  isxmet2d  24155  xmettri  24179  xmetres2  24189  bldisj  24226  blss2ps  24231  blss2  24232  xmstri2  24294  mstri2  24295  xmstri  24296  mstri  24297  xmstri3  24298  mstri3  24299  msrtri  24300  comet  24344  stdbdbl  24348  met2ndci  24353  ngprcan  24441  ngplcan  24442  ngpsubcan  24445  nmtri2  24458  nrgdsdi  24504  nrgdsdir  24505  nlmdsdi  24520  nlmdsdir  24521  blcvx  24636  icoopnst  24785  pi1grplem  24898  clmpm1dir  24952  cmodscmulexp  24971  cvsdiv  24981  cvsdivcl  24982  cphdivcl  25032  cphsubdir  25058  cphsubdi  25059  tcphcph  25087  bcthlem5  25178  volfiniun  25398  volcn  25457  itg1val2  25535  dvconst  25768  dvlip  25848  ftc1a  25894  ulmval  26233  ulmdvlem3  26255  ang180  26662  cvxcl  26833  scvxcvx  26834  sgmmul  27050  dchrabl  27103  gausslemma2dlem1a  27214  nosupbnd1  27563  noinfbnd1lem5  27576  noinfbnd1  27578  ssltss2  27638  addscom  27799  motgrp  28263  iscgra1  28530  cgrane1  28532  cgrane3  28534  cgrahl1  28536  cgrahl2  28537  cgracgr  28538  cgratr  28543  cgrabtwn  28546  cgrahl  28547  dfcgra2  28550  sacgr  28551  f1otrge  28592  colinearalglem1  28633  axcgrtr  28642  axeuclidlem  28689  axcontlem3  28693  axcontlem4  28694  axcontlem7  28697  eengtrkg  28713  eengtrkge  28714  edglnl  28872  subgruhgredgd  29010  nbfusgrlevtxm2  29104  lfgriswlk  29414  wwlknbp1  29567  umgrwwlks2on  29680  rusgrnumwwlks  29697  clwlkclwwlkfo  29731  3spthd  29898  3vfriswmgr  30000  frgr2wwlkeqm  30053  numclwwlk1lem2f  30077  numclwwlk2  30103  numclwwlk3  30107  numclwwlk5  30110  grpomuldivass  30263  ablomuldiv  30274  ablodivdiv4  30276  ablonnncan1  30279  nvmdi  30370  dipassr  30568  archiabllem2c  32809  dvrcan5  32851  reofld  32925  eqgvscpbl  32931  qusvsval  32933  quslmod  32939  quslmhm  32940  prmidlc  33036  ssmxidl  33059  ply1degltlss  33133  r1plmhm  33146  drgextlsp  33159  ccfldsrarelvec  33225  pstmfval  33365  qqhval2lem  33450  qqhvq  33456  measdivcst  33711  measdivcstALTV  33712  carsggect  33806  tgoldbachgtd  34163  bnj1098  34283  bnj149  34375  bnj1118  34484  erdszelem9  34679  resconn  34726  cvmseu  34756  cvmlift2lem10  34792  cvmlift2lem12  34794  ex-sategoelel  34901  elmrsubrn  35000  mclsind  35050  cgrid2  35470  segconeu  35478  btwncomim  35480  btwnswapid  35484  trisegint  35495  cgrxfr  35522  brofs2  35544  endofsegid  35552  btwnconn2  35569  seglemin  35580  segletr  35581  btwnsegle  35584  colinbtwnle  35585  broutsideof2  35589  btwnoutside  35592  broutsideof3  35593  outsideoftr  35596  outsidele  35599  fvray  35608  fvline  35611  ellines  35619  broucube  37012  ftc1anc  37059  sdclem1  37101  sstotbnd2  37132  iscringd  37356  lsmsat  38368  lfladdcl  38431  lflnegcl  38435  lflvscl  38437  eqlkr  38459  lshpkrlem4  38473  lshpkrlem6  38475  ldualgrplem  38505  lduallmodlem  38512  latmassOLD  38589  latm12  38590  latm32  38591  latmrot  38592  latmmdiN  38594  latmmdir  38595  omlfh1N  38618  omlfh3N  38619  cvrnbtwn2  38635  cvlexchb1  38690  cvlsupr2  38703  hlatjass  38730  hlatj12  38731  hlatj32  38732  cvrat  38783  cvrat2  38790  atltcvr  38796  atexchltN  38802  cvrat3  38803  cvrat4  38804  atbtwnexOLDN  38808  atbtwnex  38809  3dimlem3  38822  3dimlem3OLDN  38823  3at  38851  2atneat  38876  llncmp  38883  2at0mat0  38886  2atmat0  38887  llncvrlpln  38919  lplncmp  38923  2llnjaN  38927  4atlem11  38970  lplncvrlvol  38977  lvolcmp  38978  2atm2atN  39146  elpaddatriN  39164  paddasslem8  39188  paddass  39199  padd12N  39200  paddssw2  39205  paddss  39206  pmod1i  39209  pmodN  39211  pmapjlln1  39216  atmod1i1  39218  atmod1i2  39220  pexmidlem2N  39332  pl42lem2N  39341  pl42lem3N  39342  pl42lem4N  39343  pl42N  39344  lhpm0atN  39390  lautlt  39452  lautcvr  39453  lautj  39454  lautm  39455  ltrneq2  39509  cdlemd1  39559  cdleme1b  39587  cdleme1  39588  cdleme2  39589  cdleme3e  39593  cdlemefr27cl  39764  cdlemefs27cl  39774  cdleme42ke  39846  cdleme42mN  39848  cdlemf2  39923  cdlemftr2  39927  trljco  40101  tgrpgrplem  40110  tendoplass  40144  tendodi1  40145  tendodi2  40146  cdlemk34  40271  cdlemk36  40274  erngdvlem3-rN  40359  tendospdi1  40381  dialss  40407  dvhvaddass  40458  dvhopvsca  40463  dvhlveclem  40469  diblss  40531  diclss  40554  diclspsn  40555  cdlemn11pre  40571  dihmeetlem12N  40679  dihmeetlem16N  40683  dihmeetlem17N  40684  dihmeetlem18N  40685  dvh4dimN  40808  lpolconN  40848  dochpolN  40851  lclkr  40894  lclkrs  40900  lcfr  40946  irrapxlem6  42054  jm2.26lem3  42229  dgrsub2  42366  mpaaroot  42386  mendring  42423  mendlmod  42424  mendassa  42425  relexpmulg  42950  iunrelexpmin2  42952  relexpxpmin  42957  neicvgel1  43359  grumnud  43534  rfcnpre3  44206  fmuldfeq  44784  xlimbr  45028  stoweidlem43  45244  stoweidlem52  45253  stoweidlem53  45254  stoweidlem56  45257  stoweidlem57  45258  stoweidlem60  45261  issmfle  45946  issmfgt  45957  issmfge  45971  smflimlem4  45975  ltsubsubaddltsub  46494  iccpartigtl  46576  iccelpart  46586  prproropf1olem1  46656  fpprel2  46894  upgrwlkupwlk  47003  copissgrp  47031  cznrng  47124  funcringcsetcALTV2lem9  47161  funcringcsetclem9ALTV  47184  ldepsprlem  47341  lincresunit3  47350  lincreslvec3  47351  itsclc0yqe  47635  itsclc0yqsol  47638  topdlat  47817  catprs  47819  endmndlem  47823  idmon  47824  idepi  47825  thincmon  47842  thincepi  47843  functhinclem1  47849  grptcmon  47904  grptcepi  47905