Theorem simprr 533

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜒 → 𝜒)
2	1	ad2antll 491	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  dfifp2dc  989  simp1rr  1089  simp2rr  1093  simp3rr  1097  elpr2elpr  3860  invdisjrab  4083  disjiun  4084  reg2exmidlema  4634  reg3exmidlemwe  4679  nnsucpred  4717  iotam  5320  fvmptt  5741  fcof1  5929  fliftfun  5942  isotr  5962  riotass2  6005  acexmidlemab  6017  ovmpodf  6158  fnmpoovd  6385  1stconst  6391  2ndconst  6392  cnvf1olem  6394  f1od2  6405  smoiso  6473  tfrcldm  6534  tfrcl  6535  nntr2  6676  swoer  6735  erinxp  6783  ecopovsymg  6808  th3qlem1  6811  f1imaen2g  6972  pw2f1odclem  7025  mapdom1g  7038  fict  7060  fidifsnen  7062  dif1enen  7074  fiunsnnn  7075  fisbth  7077  findcard2d  7085  findcard2sd  7086  diffifi  7088  ac6sfi  7092  fimax2gtri  7096  nnwetri  7113  unsnfi  7116  unsnfidcex  7117  unsnfidcel  7118  fisseneq  7132  ssfirab  7134  exmidssfi  7136  fidcenumlemrk  7158  fidcenumlemr  7159  sbthlemi6  7166  sbthlemi8  7168  isbth  7171  fiuni  7182  supmaxti  7208  infminti  7231  ordiso2  7239  eldju2ndl  7276  eldju2ndr  7277  omp1eomlem  7298  difinfsnlem  7303  difinfinf  7305  ctmlemr  7312  ctssdccl  7315  nninfninc  7327  fodjum  7350  fodju0  7351  omniwomnimkv  7371  exmidfodomrlemrALT  7419  acfun  7427  exmidaclem  7428  netap  7478  exmidmotap  7485  ccfunen  7488  cc1  7489  cc2lem  7490  dfplpq2  7579  dfmpq2  7580  mulpipqqs  7598  distrnqg  7612  enq0sym  7657  enq0tr  7659  distrnq0  7684  prarloclem3  7722  genplt2i  7735  addlocpr  7761  prmuloc  7791  distrlem1prl  7807  distrlem1pru  7808  ltexprlemopl  7826  ltexprlemopu  7828  ltexprlemfl  7834  ltexprlemrl  7835  ltexprlemfu  7836  ltexprlemru  7837  addcanprleml  7839  addcanprlemu  7840  ltaprg  7844  prplnqu  7845  addextpr  7846  recexprlemdisj  7855  recexprlemloc  7856  aptiprleml  7864  aptiprlemu  7865  ltmprr  7867  archpr  7868  cauappcvgprlemopl  7871  cauappcvgprlemopu  7873  cauappcvgprlemdisj  7876  cauappcvgprlemloc  7877  cauappcvgprlem1  7884  cauappcvgprlemlim  7886  caucvgprlemnkj  7891  caucvgprlemopl  7894  caucvgprlemopu  7896  caucvgprlemdisj  7899  caucvgprlemloc  7900  caucvgprprlemnkltj  7914  caucvgprprlemnkeqj  7915  caucvgprprlemnjltk  7916  caucvgprprlemml  7919  caucvgprprlemmu  7920  caucvgprprlemopl  7922  caucvgprprlemopu  7924  caucvgprprlemdisj  7927  caucvgprprlemloc  7928  caucvgprprlemaddq  7933  suplocexprlemrl  7942  suplocexprlemmu  7943  suplocexprlemru  7944  suplocexprlemdisj  7945  suplocexprlemloc  7946  suplocexprlemex  7947  suplocexprlemub  7948  recexgt0sr  7998  mulgt0sr  8003  prsrriota  8013  suplocsrlem  8033  addcnsr  8059  mulcnsr  8060  mulcnsrec  8068  axmulcom  8096  rereceu  8114  axarch  8116  axcaucvglemres  8124  axpre-suploclemres  8126  lelttr  8273  ltletr  8274  addcan  8364  addcan2  8365  addsub4  8427  ltadd2  8604  le2add  8629  lt2add  8630  lt2sub  8645  le2sub  8646  eqord1  8668  rereim  8771  apreap  8772  apreim  8788  mulreim  8789  apcotr  8792  apadd1  8793  addext  8795  apneg  8796  mulext1  8797  mulext  8799  ltleap  8817  aprcl  8831  mulap0  8839  mulcanapd  8846  recapb  8856  rec11ap  8895  rec11rap  8896  divdivdivap  8898  ddcanap  8911  divadddivap  8912  prodgt0gt0  9036  prodgt0  9037  prodge0  9039  lemulge11  9051  lt2mul2div  9064  ltrec  9068  lerec  9069  lerec2  9074  ledivp1  9088  mulle0r  9129  nn0ge0div  9572  suprzclex  9583  qapne  9878  xrlelttr  10046  xrltletr  10047  xrre3  10062  xrrege0  10065  xaddge0  10118  xle2add  10119  xlt2add  10120  fzass4  10302  fzrev  10324  elfz1b  10330  eluzgtdifelfzo  10448  fzocatel  10450  zsupcllemstep  10495  zsupcllemex  10496  zssinfcl  10498  suprzubdc  10502  exbtwnzlemex  10515  rebtwn2z  10520  modqid  10617  modqcyc  10627  modqaddabs  10630  modqaddmod  10631  mulqaddmodid  10632  modqadd2mod  10642  modqltm1p1mod  10644  modqsubmod  10650  modqsubmodmod  10651  modaddmodup  10655  modqmulmod  10657  modqmulmodr  10658  modqaddmulmod  10659  modqsubdir  10661  frec2uzisod  10675  uzennn  10704  iseqovex  10726  seqvalcd  10729  seq1g  10731  seqf  10732  seqovcd  10735  seqclg  10740  seqm1g  10742  seq3shft2  10749  seqshft2g  10750  monoord  10753  iseqf1olemnab  10769  seqf1oglem1  10787  seqf1og  10789  seqhomog  10798  seqfeq4g  10799  seq3distr  10800  expnegzap  10841  ltexp2a  10859  le2sq2  10883  bernneq  10928  expnlbnd2  10933  nn0ltexp2  10977  nn0opth2  10992  faclbnd  11009  bcval5  11031  hashcl  11049  hashen  11052  fihashdom  11072  hashunlem  11073  hashun  11074  hashxp  11096  fimaxq  11097  zfz1isolem1  11110  zfz1iso  11111  seq3coll  11112  sswrd  11131  ccatw2s1p1g  11231  ccatw2s1p2  11232  ccat2s1fstg  11234  wrdind  11312  pfxccatin12lem1  11318  pfxccatin12lem3  11322  reuccatpfxs1lem  11336  cvg1nlemres  11568  cvg1n  11569  resqrexlemp1rp  11589  resqrexlemoverl  11604  resqrexlemex  11608  sqrtsq  11627  abslt  11671  absle  11672  abs3lem  11694  maxleastlt  11798  maxltsup  11801  fimaxre2  11810  negfi  11811  xrmaxleastlt  11839  xrmaxltsup  11841  xrmaxaddlem  11843  2clim  11884  climcn2  11892  addcn2  11893  mulcn2  11895  reccn2ap  11896  climge0  11908  climcau  11930  fzf1o  11959  summodclem2  11966  summodc  11967  zsumdc  11968  fsumf1o  11974  fisumss  11976  fsum3cvg3  11980  fsumcl2lem  11982  fsumadd  11990  mptfzshft  12026  fsumrev  12027  fsummulc2  12032  fsumconst  12038  modfsummod  12042  fsumrelem  12055  binom  12068  cvgratnn  12115  mertenslemub  12118  prodmodclem2  12161  prodmodc  12162  zproddc  12163  fprodf1o  12172  fprodssdc  12174  fprodmul  12175  fprodcl2lem  12189  fprodrev  12203  fprodconst  12204  fprodap0  12205  fprodrec  12213  fprodap0f  12220  fprodle  12224  fprodmodd  12225  efcllem  12243  tanaddaplem  12322  moddvds  12383  dvdsflip  12435  oexpneg  12461  nn0o  12491  fldivndvdslt  12521  bitsfi  12541  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlemeu  12601  dfgcd3  12604  dfgcd2  12608  dvdsmulgcd  12619  bezoutr  12626  nninfctlemfo  12634  lcmgcdlem  12672  coprmdvds2  12688  qredeu  12692  rpdvds  12694  cncongr1  12698  prmind2  12715  isprm5lem  12736  isprm6  12742  oddpwdclemdc  12768  nonsq  12802  hashdvds  12816  crth  12819  eulerthlemh  12826  prmdiveq  12831  hashgcdlem  12833  hashgcdeq  12835  nnnn0modprm0  12851  pclemub  12883  pceu  12891  pcmul  12897  pcqmul  12899  pcgcd1  12924  pc2dvds  12926  difsqpwdvds  12934  pcmpt  12939  prmpwdvds  12951  1arith  12963  mul4sq  12990  4sqlemafi  12991  4sqlemffi  12992  4sqexercise2  12995  ennnfonelemg  13047  ennnfonelemex  13058  ennnfonelemrnh  13060  ennnfonelemf1  13062  ennnfonelemrn  13063  ennnfonelemdm  13064  ennnfonelemim  13068  ennnfone  13069  ctinf  13074  ctiunctlemfo  13083  nninfdclemcl  13092  nninfdclemf  13093  nninfdclemp1  13094  unbendc  13098  isstruct2r  13116  setscom  13145  ercpbl  13437  opifismgmdc  13477  grpinvalem  13491  igsumvalx  13495  gsumfzval  13497  gsumval2  13503  sgrppropd  13519  prdssgrpd  13521  mndpropd  13546  issubmnd  13548  submnd0  13550  prdsmndd  13554  mhmf1o  13576  subsubm  13589  0mhm  13592  resmhm  13593  mhmco  13596  mhmima  13597  mhmeql  13598  gsumfzz  13601  gsumwsubmcl  13602  gsumfzcl  13605  grprcan  13643  grpinvid1  13658  grpinvid2  13659  grplcan  13668  grplmulf1o  13680  grpnpncan0  13702  dfgrp3mlem  13704  grplactcnv  13708  pwssub  13719  mulgval  13732  mulgfng  13734  mulgnngsum  13737  mulg1  13739  mulgnnp1  13740  mulgneg  13750  mulgnndir  13761  mulgdirlem  13763  mulgnn0ass  13768  mulgass  13769  subgmulg  13798  issubg4m  13803  subsubg  13807  subgintm  13808  isnsg3  13817  eqgcpbl  13838  ghmeql  13877  ghmnsgima  13878  ghmnsgpreima  13879  ghmf1  13883  ghmf1o  13885  conjghm  13886  qusghm  13892  ablpncan3  13927  invghm  13939  eqgabl  13940  gsumfzreidx  13947  gsumfzsubmcl  13948  gsumfzmptfidmadd  13949  gsumfzmhm  13953  rngpropd  13992  imasrng  13993  qusrng  13995  srglmhm  14030  srgrmhm  14031  ringpropd  14075  ringlghm  14098  ringrghm  14099  imasring  14101  qusring2  14103  opprrngbg  14115  dvdsrvald  14131  dvdsrd  14132  dvdsrex  14136  dvdsrtr  14139  unitpropdg  14186  rhmopp  14214  isnzr2  14222  issubrng2  14248  subrngintm  14250  subsubrng  14252  subrgintm  14281  subsubrg  14283  rhmpropd  14292  aprap  14324  lmodprop2d  14386  rmodislmod  14389  lssvacl  14403  lssvsubcl  14404  lssvscl  14413  islss3  14417  lss1d  14421  rnglidlmcl  14518  2idlcpblrng  14561  crngridl  14568  expghmap  14645  mulgghm2  14646  mulgrhm  14647  znf1o  14689  znleval  14691  znidom  14695  znidomb  14696  znunit  14697  psrbagcon  14714  mplsubgfilemcl  14742  iuncld  14868  ssnei2  14910  topssnei  14915  restopnb  14934  cnfval  14947  cnpfval  14948  iscnp4  14971  cnptopco  14975  cncnpi  14981  cncnp  14983  cnconst2  14986  cnrest2  14989  cnptoprest  14992  cnptoprest2  14993  cnpdis  14995  lmss  14999  lmtopcnp  15003  neitx  15021  txcnp  15024  txrest  15029  txdis1cn  15031  txlm  15032  cnmpt21  15044  imasnopn  15052  xmetres2  15132  blvalps  15141  blval  15142  elbl2ps  15145  elbl2  15146  blhalf  15161  blssexps  15182  blssex  15183  ssblex  15184  blin2  15185  bdmetval  15253  xmetxp  15260  xmettx  15263  metcnpi3  15270  txmetcnp  15271  addcncntoplem  15314  fsumcncntop  15320  elcncf2  15327  mulc1cncf  15342  cncfco  15344  cncfmet  15345  cncfmptc  15349  mulcncf  15361  dedekindeulemub  15371  dedekindeulemloc  15372  dedekindeulemlu  15374  dedekindeu  15376  dedekindicclemub  15380  dedekindicclemloc  15381  dedekindicclemlu  15383  dedekindicclemicc  15385  dedekindicc  15386  ivthinclemlopn  15389  ivthinclemuopn  15391  dich0  15405  limcimo  15418  cnplimccntop  15423  limccnp2lem  15429  limccnp2cntop  15430  dvfvalap  15434  dveflem  15479  plycolemc  15511  plyco  15512  plyrecj  15516  reeff1olem  15524  reeff1oleme  15525  eflt  15528  sin0pilem2  15535  pilem3  15536  ioocosf1o  15607  cxplt  15669  cxple  15670  cxplt3  15673  apcxp2  15692  rprelogbmul  15708  rprelogbdiv  15710  logbgt0b  15719  logbgcd1irrap  15723  mpodvdsmulf1o  15743  fsumdvdsmul  15744  lgsdir2lem5  15790  lgsdi  15795  lgsne0  15796  gausslemma2dlem1f1o  15818  lgseisenlem2  15829  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  lgsquad2lem2  15840  lgsquad2  15841  2sqlem6  15878  2sqlem8  15881  2sqlem9  15882  2sqlem10  15883  upgredg  16024  usgredg4  16095  uspgredg2vlem  16100  usgr1eop  16125  upgrspanop  16163  umgrspanop  16164  usgrspanop  16165  vtxedgfi  16169  vtxlpfi  16170  iswlkg  16209  upgriswlkdc  16240  upgr2wlkdc  16257  clwwlkccatlem  16280  clwwlknonex2e  16320  nnti  16651  pwtrufal  16658  pwf1oexmid  16660  sssneq  16663  qdencn  16694  cvgcmp2n  16704  trilpolemlt1  16712  trirec0  16715  qdiff  16720  redc0  16729  reap0  16730  cndcap  16731  nconstwlpolemgt0  16736  neap0mkv  16741  supfz  16743  inffz  16744  gfsumval  16748  gfsumcl  16755