Theorem simprr 531

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:  simp1rr  1068  simp2rr  1072  simp3rr  1076  elpr2elpr  3833  invdisjrab  4056  disjiun  4057  reg2exmidlema  4603  reg3exmidlemwe  4648  nnsucpred  4686  iotam  5286  fvmptt  5699  fcof1  5880  fliftfun  5893  isotr  5913  riotass2  5956  acexmidlemab  5968  ovmpodf  6107  fnmpoovd  6331  1stconst  6337  2ndconst  6338  cnvf1olem  6340  f1od2  6351  smoiso  6418  tfrcldm  6479  tfrcl  6480  nntr2  6619  swoer  6678  erinxp  6726  ecopovsymg  6751  th3qlem1  6754  f1imaen2g  6915  pw2f1odclem  6963  mapdom1g  6976  fict  6998  fidifsnen  7000  dif1enen  7010  fiunsnnn  7011  fisbth  7013  findcard2d  7021  findcard2sd  7022  diffifi  7024  ac6sfi  7028  fimax2gtri  7031  nnwetri  7046  unsnfi  7049  unsnfidcex  7050  unsnfidcel  7051  fisseneq  7064  ssfirab  7066  fidcenumlemrk  7089  fidcenumlemr  7090  sbthlemi6  7097  sbthlemi8  7099  isbth  7102  fiuni  7113  supmaxti  7139  infminti  7162  ordiso2  7170  eldju2ndl  7207  eldju2ndr  7208  omp1eomlem  7229  difinfsnlem  7234  difinfinf  7236  ctmlemr  7243  ctssdccl  7246  nninfninc  7258  fodjum  7281  fodju0  7282  omniwomnimkv  7302  exmidfodomrlemrALT  7349  acfun  7357  exmidaclem  7358  netap  7408  exmidmotap  7415  ccfunen  7418  cc1  7419  cc2lem  7420  dfplpq2  7509  dfmpq2  7510  mulpipqqs  7528  distrnqg  7542  enq0sym  7587  enq0tr  7589  distrnq0  7614  prarloclem3  7652  genplt2i  7665  addlocpr  7691  prmuloc  7721  distrlem1prl  7737  distrlem1pru  7738  ltexprlemopl  7756  ltexprlemopu  7758  ltexprlemfl  7764  ltexprlemrl  7765  ltexprlemfu  7766  ltexprlemru  7767  addcanprleml  7769  addcanprlemu  7770  ltaprg  7774  prplnqu  7775  addextpr  7776  recexprlemdisj  7785  recexprlemloc  7786  aptiprleml  7794  aptiprlemu  7795  ltmprr  7797  archpr  7798  cauappcvgprlemopl  7801  cauappcvgprlemopu  7803  cauappcvgprlemdisj  7806  cauappcvgprlemloc  7807  cauappcvgprlem1  7814  cauappcvgprlemlim  7816  caucvgprlemnkj  7821  caucvgprlemopl  7824  caucvgprlemopu  7826  caucvgprlemdisj  7829  caucvgprlemloc  7830  caucvgprprlemnkltj  7844  caucvgprprlemnkeqj  7845  caucvgprprlemnjltk  7846  caucvgprprlemml  7849  caucvgprprlemmu  7850  caucvgprprlemopl  7852  caucvgprprlemopu  7854  caucvgprprlemdisj  7857  caucvgprprlemloc  7858  caucvgprprlemaddq  7863  suplocexprlemrl  7872  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemex  7877  suplocexprlemub  7878  recexgt0sr  7928  mulgt0sr  7933  prsrriota  7943  suplocsrlem  7963  addcnsr  7989  mulcnsr  7990  mulcnsrec  7998  axmulcom  8026  rereceu  8044  axarch  8046  axcaucvglemres  8054  axpre-suploclemres  8056  lelttr  8203  ltletr  8204  addcan  8294  addcan2  8295  addsub4  8357  ltadd2  8534  le2add  8559  lt2add  8560  lt2sub  8575  le2sub  8576  eqord1  8598  rereim  8701  apreap  8702  apreim  8718  mulreim  8719  apcotr  8722  apadd1  8723  addext  8725  apneg  8726  mulext1  8727  mulext  8729  ltleap  8747  aprcl  8761  mulap0  8769  mulcanapd  8776  recapb  8786  rec11ap  8825  rec11rap  8826  divdivdivap  8828  ddcanap  8841  divadddivap  8842  prodgt0gt0  8966  prodgt0  8967  prodge0  8969  lemulge11  8981  lt2mul2div  8994  ltrec  8998  lerec  8999  lerec2  9004  ledivp1  9018  mulle0r  9059  nn0ge0div  9502  suprzclex  9513  qapne  9802  xrlelttr  9970  xrltletr  9971  xrre3  9986  xrrege0  9989  xaddge0  10042  xle2add  10043  xlt2add  10044  fzass4  10226  fzrev  10248  elfz1b  10254  eluzgtdifelfzo  10370  fzocatel  10372  zsupcllemstep  10416  zsupcllemex  10417  zssinfcl  10419  suprzubdc  10423  exbtwnzlemex  10436  rebtwn2z  10441  modqid  10538  modqcyc  10548  modqaddabs  10551  modqaddmod  10552  mulqaddmodid  10553  modqadd2mod  10563  modqltm1p1mod  10565  modqsubmod  10571  modqsubmodmod  10572  modaddmodup  10576  modqmulmod  10578  modqmulmodr  10579  modqaddmulmod  10580  modqsubdir  10582  frec2uzisod  10596  uzennn  10625  iseqovex  10647  seqvalcd  10650  seq1g  10652  seqf  10653  seqovcd  10656  seqclg  10661  seqm1g  10663  seq3shft2  10670  seqshft2g  10671  monoord  10674  iseqf1olemnab  10690  seqf1oglem1  10708  seqf1og  10710  seqhomog  10719  seqfeq4g  10720  seq3distr  10721  expnegzap  10762  ltexp2a  10780  le2sq2  10804  bernneq  10849  expnlbnd2  10854  nn0ltexp2  10898  nn0opth2  10913  faclbnd  10930  bcval5  10952  hashcl  10970  hashen  10973  fihashdom  10992  hashunlem  10993  hashun  10994  hashxp  11015  fimaxq  11016  zfz1isolem1  11029  zfz1iso  11030  seq3coll  11031  sswrd  11047  ccatw2s1p2  11142  wrdind  11220  pfxccatin12lem1  11226  pfxccatin12lem3  11230  reuccatpfxs1lem  11244  cvg1nlemres  11462  cvg1n  11463  resqrexlemp1rp  11483  resqrexlemoverl  11498  resqrexlemex  11502  sqrtsq  11521  abslt  11565  absle  11566  abs3lem  11588  maxleastlt  11692  maxltsup  11695  fimaxre2  11704  negfi  11705  xrmaxleastlt  11733  xrmaxltsup  11735  xrmaxaddlem  11737  2clim  11778  climcn2  11786  addcn2  11787  mulcn2  11789  reccn2ap  11790  climge0  11802  climcau  11824  summodclem2  11859  summodc  11860  zsumdc  11861  fsumf1o  11867  fisumss  11869  fsum3cvg3  11873  fsumcl2lem  11875  fsumadd  11883  mptfzshft  11919  fsumrev  11920  fsummulc2  11925  fsumconst  11931  modfsummod  11935  fsumrelem  11948  binom  11961  cvgratnn  12008  mertenslemub  12011  prodmodclem2  12054  prodmodc  12055  zproddc  12056  fprodf1o  12065  fprodssdc  12067  fprodmul  12068  fprodcl2lem  12082  fprodrev  12096  fprodconst  12097  fprodap0  12098  fprodrec  12106  fprodap0f  12113  fprodle  12117  fprodmodd  12118  efcllem  12136  tanaddaplem  12215  moddvds  12276  dvdsflip  12328  oexpneg  12354  nn0o  12384  fldivndvdslt  12414  bitsfi  12434  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemeu  12494  dfgcd3  12497  dfgcd2  12501  dvdsmulgcd  12512  bezoutr  12519  nninfctlemfo  12527  lcmgcdlem  12565  coprmdvds2  12581  qredeu  12585  rpdvds  12587  cncongr1  12591  prmind2  12608  isprm5lem  12629  isprm6  12635  oddpwdclemdc  12661  nonsq  12695  hashdvds  12709  crth  12712  eulerthlemh  12719  prmdiveq  12724  hashgcdlem  12726  hashgcdeq  12728  nnnn0modprm0  12744  pclemub  12776  pceu  12784  pcmul  12790  pcqmul  12792  pcgcd1  12817  pc2dvds  12819  difsqpwdvds  12827  pcmpt  12832  prmpwdvds  12844  1arith  12856  mul4sq  12883  4sqlemafi  12884  4sqlemffi  12885  4sqexercise2  12888  ennnfonelemg  12940  ennnfonelemex  12951  ennnfonelemrnh  12953  ennnfonelemf1  12955  ennnfonelemrn  12956  ennnfonelemdm  12957  ennnfonelemim  12961  ennnfone  12962  ctinf  12967  ctiunctlemfo  12976  nninfdclemcl  12985  nninfdclemf  12986  nninfdclemp1  12987  unbendc  12991  isstruct2r  13009  setscom  13038  ercpbl  13330  opifismgmdc  13370  grpinvalem  13384  igsumvalx  13388  gsumfzval  13390  gsumval2  13396  sgrppropd  13412  prdssgrpd  13414  mndpropd  13439  issubmnd  13441  submnd0  13443  prdsmndd  13447  mhmf1o  13469  subsubm  13482  0mhm  13485  resmhm  13486  mhmco  13489  mhmima  13490  mhmeql  13491  gsumfzz  13494  gsumwsubmcl  13495  gsumfzcl  13498  grprcan  13536  grpinvid1  13551  grpinvid2  13552  grplcan  13561  grplmulf1o  13573  grpnpncan0  13595  dfgrp3mlem  13597  grplactcnv  13601  pwssub  13612  mulgval  13625  mulgfng  13627  mulgnngsum  13630  mulg1  13632  mulgnnp1  13633  mulgneg  13643  mulgnndir  13654  mulgdirlem  13656  mulgnn0ass  13661  mulgass  13662  subgmulg  13691  issubg4m  13696  subsubg  13700  subgintm  13701  isnsg3  13710  eqgcpbl  13731  ghmeql  13770  ghmnsgima  13771  ghmnsgpreima  13772  ghmf1  13776  ghmf1o  13778  conjghm  13779  qusghm  13785  ablpncan3  13820  invghm  13832  eqgabl  13833  gsumfzreidx  13840  gsumfzsubmcl  13841  gsumfzmptfidmadd  13842  gsumfzmhm  13846  rngpropd  13884  imasrng  13885  qusrng  13887  srglmhm  13922  srgrmhm  13923  ringpropd  13967  ringlghm  13990  ringrghm  13991  imasring  13993  qusring2  13995  opprrngbg  14007  dvdsrvald  14022  dvdsrd  14023  dvdsrex  14027  dvdsrtr  14030  unitpropdg  14077  rhmopp  14105  isnzr2  14113  issubrng2  14139  subrngintm  14141  subsubrng  14143  subrgintm  14172  subsubrg  14174  rhmpropd  14183  aprap  14215  lmodprop2d  14277  rmodislmod  14280  lssvacl  14294  lssvsubcl  14295  lssvscl  14304  islss3  14308  lss1d  14312  rnglidlmcl  14409  2idlcpblrng  14452  crngridl  14459  expghmap  14536  mulgghm2  14537  mulgrhm  14538  znf1o  14580  znleval  14582  znidom  14586  znidomb  14587  znunit  14588  mplsubgfilemcl  14628  iuncld  14754  ssnei2  14796  topssnei  14801  restopnb  14820  cnfval  14833  cnpfval  14834  iscnp4  14857  cnptopco  14861  cncnpi  14867  cncnp  14869  cnconst2  14872  cnrest2  14875  cnptoprest  14878  cnptoprest2  14879  cnpdis  14881  lmss  14885  lmtopcnp  14889  neitx  14907  txcnp  14910  txrest  14915  txdis1cn  14917  txlm  14918  cnmpt21  14930  imasnopn  14938  xmetres2  15018  blvalps  15027  blval  15028  elbl2ps  15031  elbl2  15032  blhalf  15047  blssexps  15068  blssex  15069  ssblex  15070  blin2  15071  bdmetval  15139  xmetxp  15146  xmettx  15149  metcnpi3  15156  txmetcnp  15157  addcncntoplem  15200  fsumcncntop  15206  elcncf2  15213  mulc1cncf  15228  cncfco  15230  cncfmet  15231  cncfmptc  15235  mulcncf  15247  dedekindeulemub  15257  dedekindeulemloc  15258  dedekindeulemlu  15260  dedekindeu  15262  dedekindicclemub  15266  dedekindicclemloc  15267  dedekindicclemlu  15269  dedekindicclemicc  15271  dedekindicc  15272  ivthinclemlopn  15275  ivthinclemuopn  15277  dich0  15291  limcimo  15304  cnplimccntop  15309  limccnp2lem  15315  limccnp2cntop  15316  dvfvalap  15320  dveflem  15365  plycolemc  15397  plyco  15398  plyrecj  15402  reeff1olem  15410  reeff1oleme  15411  eflt  15414  sin0pilem2  15421  pilem3  15422  ioocosf1o  15493  cxplt  15555  cxple  15556  cxplt3  15559  apcxp2  15578  rprelogbmul  15594  rprelogbdiv  15596  logbgt0b  15605  logbgcd1irrap  15609  mpodvdsmulf1o  15629  fsumdvdsmul  15630  lgsdir2lem5  15676  lgsdi  15681  lgsne0  15682  gausslemma2dlem1f1o  15704  lgseisenlem2  15715  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2lem2  15726  lgsquad2  15727  2sqlem6  15764  2sqlem8  15767  2sqlem9  15768  2sqlem10  15769  upgredg  15907  usgredg4  15978  uspgredg2vlem  15983  nnti  16267  pwtrufal  16274  pwf1oexmid  16276  sssneq  16279  qdencn  16306  cvgcmp2n  16312  trilpolemlt1  16320  trirec0  16323  redc0  16336  reap0  16337  cndcap  16338  nconstwlpolemgt0  16343  neap0mkv  16348  supfz  16350  inffz  16351