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  1065  simp2rr  1069  simp3rr  1073  disjiun  4013  reg2exmidlema  4551  reg3exmidlemwe  4596  nnsucpred  4634  iotam  5227  fvmptt  5628  fcof1  5805  fliftfun  5818  isotr  5838  riotass2  5879  acexmidlemab  5891  ovmpodf  6029  fnmpoovd  6241  1stconst  6247  2ndconst  6248  cnvf1olem  6250  f1od2  6261  smoiso  6328  tfrcldm  6389  tfrcl  6390  nntr2  6529  swoer  6588  erinxp  6636  ecopovsymg  6661  th3qlem1  6664  f1imaen2g  6820  pw2f1odclem  6863  mapdom1g  6876  fict  6897  fidifsnen  6899  dif1enen  6909  fiunsnnn  6910  fisbth  6912  findcard2d  6920  findcard2sd  6921  diffifi  6923  ac6sfi  6927  fimax2gtri  6930  nnwetri  6945  unsnfi  6948  unsnfidcex  6949  unsnfidcel  6950  fisseneq  6961  ssfirab  6963  fidcenumlemrk  6984  fidcenumlemr  6985  sbthlemi6  6992  sbthlemi8  6994  isbth  6997  fiuni  7008  supmaxti  7034  infminti  7057  ordiso2  7065  eldju2ndl  7102  eldju2ndr  7103  omp1eomlem  7124  difinfsnlem  7129  difinfinf  7131  ctmlemr  7138  ctssdccl  7141  fodjum  7175  fodju0  7176  omniwomnimkv  7196  exmidfodomrlemrALT  7233  acfun  7237  exmidaclem  7238  netap  7284  exmidmotap  7291  ccfunen  7294  cc1  7295  cc2lem  7296  dfplpq2  7384  dfmpq2  7385  mulpipqqs  7403  distrnqg  7417  enq0sym  7462  enq0tr  7464  distrnq0  7489  prarloclem3  7527  genplt2i  7540  addlocpr  7566  prmuloc  7596  distrlem1prl  7612  distrlem1pru  7613  ltexprlemopl  7631  ltexprlemopu  7633  ltexprlemfl  7639  ltexprlemrl  7640  ltexprlemfu  7641  ltexprlemru  7642  addcanprleml  7644  addcanprlemu  7645  ltaprg  7649  prplnqu  7650  addextpr  7651  recexprlemdisj  7660  recexprlemloc  7661  aptiprleml  7669  aptiprlemu  7670  ltmprr  7672  archpr  7673  cauappcvgprlemopl  7676  cauappcvgprlemopu  7678  cauappcvgprlemdisj  7681  cauappcvgprlemloc  7682  cauappcvgprlem1  7689  cauappcvgprlemlim  7691  caucvgprlemnkj  7696  caucvgprlemopl  7699  caucvgprlemopu  7701  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprprlemnkltj  7719  caucvgprprlemnkeqj  7720  caucvgprprlemnjltk  7721  caucvgprprlemml  7724  caucvgprprlemmu  7725  caucvgprprlemopl  7727  caucvgprprlemopu  7729  caucvgprprlemdisj  7732  caucvgprprlemloc  7733  caucvgprprlemaddq  7738  suplocexprlemrl  7747  suplocexprlemmu  7748  suplocexprlemru  7749  suplocexprlemdisj  7750  suplocexprlemloc  7751  suplocexprlemex  7752  suplocexprlemub  7753  recexgt0sr  7803  mulgt0sr  7808  prsrriota  7818  suplocsrlem  7838  addcnsr  7864  mulcnsr  7865  mulcnsrec  7873  axmulcom  7901  rereceu  7919  axarch  7921  axcaucvglemres  7929  axpre-suploclemres  7931  lelttr  8077  ltletr  8078  addcan  8168  addcan2  8169  addsub4  8231  ltadd2  8407  le2add  8432  lt2add  8433  lt2sub  8448  le2sub  8449  eqord1  8471  rereim  8574  apreap  8575  apreim  8591  mulreim  8592  apcotr  8595  apadd1  8596  addext  8598  apneg  8599  mulext1  8600  mulext  8602  ltleap  8620  aprcl  8634  mulap0  8642  mulcanapd  8649  recapb  8659  rec11ap  8698  rec11rap  8699  divdivdivap  8701  ddcanap  8714  divadddivap  8715  prodgt0gt0  8839  prodgt0  8840  prodge0  8842  lemulge11  8854  lt2mul2div  8867  ltrec  8871  lerec  8872  lerec2  8877  ledivp1  8891  mulle0r  8932  nn0ge0div  9371  suprzclex  9382  qapne  9671  xrlelttr  9838  xrltletr  9839  xrre3  9854  xrrege0  9857  xaddge0  9910  xle2add  9911  xlt2add  9912  fzass4  10094  fzrev  10116  elfz1b  10122  eluzgtdifelfzo  10229  fzocatel  10231  exbtwnzlemex  10282  rebtwn2z  10287  modqid  10382  modqcyc  10392  modqaddabs  10395  modqaddmod  10396  mulqaddmodid  10397  modqadd2mod  10407  modqltm1p1mod  10409  modqsubmod  10415  modqsubmodmod  10416  modaddmodup  10420  modqmulmod  10422  modqmulmodr  10423  modqaddmulmod  10424  modqsubdir  10426  frec2uzisod  10440  uzennn  10469  iseqovex  10489  seqvalcd  10492  seqf  10494  seqovcd  10496  seq3shft2  10506  monoord  10509  iseqf1olemnab  10521  seqfeq4g  10546  seq3distr  10547  expnegzap  10588  ltexp2a  10606  le2sq2  10630  bernneq  10675  expnlbnd2  10680  nn0ltexp2  10724  nn0opth2  10739  faclbnd  10756  bcval5  10778  hashcl  10796  hashen  10799  fihashdom  10818  hashunlem  10819  hashun  10820  hashxp  10841  fimaxq  10842  zfz1isolem1  10855  zfz1iso  10856  seq3coll  10857  cvg1nlemres  11029  cvg1n  11030  resqrexlemp1rp  11050  resqrexlemoverl  11065  resqrexlemex  11069  sqrtsq  11088  abslt  11132  absle  11133  abs3lem  11155  maxleastlt  11259  maxltsup  11262  fimaxre2  11270  negfi  11271  xrmaxleastlt  11299  xrmaxltsup  11301  xrmaxaddlem  11303  2clim  11344  climcn2  11352  addcn2  11353  mulcn2  11355  reccn2ap  11356  climge0  11368  climcau  11390  summodclem2  11425  summodc  11426  zsumdc  11427  fsumf1o  11433  fisumss  11435  fsum3cvg3  11439  fsumcl2lem  11441  fsumadd  11449  mptfzshft  11485  fsumrev  11486  fsummulc2  11491  fsumconst  11497  modfsummod  11501  fsumrelem  11514  binom  11527  cvgratnn  11574  mertenslemub  11577  prodmodclem2  11620  prodmodc  11621  zproddc  11622  fprodf1o  11631  fprodssdc  11633  fprodmul  11634  fprodcl2lem  11648  fprodrev  11662  fprodconst  11663  fprodap0  11664  fprodrec  11672  fprodap0f  11679  fprodle  11683  fprodmodd  11684  efcllem  11702  tanaddaplem  11781  moddvds  11841  dvdsflip  11892  oexpneg  11917  nn0o  11947  fldivndvdslt  11975  zsupcllemstep  11981  zsupcllemex  11982  zssinfcl  11984  suprzubdc  11988  bezoutlemnewy  12032  bezoutlemstep  12033  bezoutlemeu  12043  dfgcd3  12046  dfgcd2  12050  dvdsmulgcd  12061  bezoutr  12068  lcmgcdlem  12112  coprmdvds2  12128  qredeu  12132  rpdvds  12134  cncongr1  12138  prmind2  12155  isprm5lem  12176  isprm6  12182  oddpwdclemdc  12208  nonsq  12242  hashdvds  12256  crth  12259  eulerthlemh  12266  prmdiveq  12271  hashgcdlem  12273  hashgcdeq  12274  nnnn0modprm0  12290  pclemub  12322  pceu  12330  pcmul  12336  pcqmul  12338  pcgcd1  12363  pc2dvds  12365  difsqpwdvds  12373  pcmpt  12378  prmpwdvds  12390  1arith  12402  mul4sq  12429  4sqlemafi  12430  4sqlemffi  12431  4sqexercise2  12434  ennnfonelemg  12457  ennnfonelemex  12468  ennnfonelemrnh  12470  ennnfonelemf1  12472  ennnfonelemrn  12473  ennnfonelemdm  12474  ennnfonelemim  12478  ennnfone  12479  ctinf  12484  ctiunctlemfo  12493  nninfdclemcl  12502  nninfdclemf  12503  nninfdclemp1  12504  unbendc  12508  isstruct2r  12526  setscom  12555  ercpbl  12810  opifismgmdc  12850  grpinvalem  12864  igsumvalx  12868  gsumval2  12875  sgrppropd  12891  mndpropd  12916  issubmnd  12918  submnd0  12920  mhmf1o  12937  subsubm  12950  0mhm  12953  resmhm  12954  mhmco  12957  mhmima  12958  mhmeql  12959  grprcan  12996  grpinvid1  13011  grpinvid2  13012  grplcan  13021  grplmulf1o  13033  grpnpncan0  13055  dfgrp3mlem  13057  grplactcnv  13061  mulgval  13079  mulgfng  13081  mulgnngsum  13084  mulg1  13086  mulgnnp1  13087  mulgneg  13097  mulgnndir  13108  mulgdirlem  13110  mulgnn0ass  13115  mulgass  13116  subgmulg  13144  issubg4m  13149  subsubg  13153  subgintm  13154  isnsg3  13163  eqgcpbl  13184  ghmeql  13223  ghmnsgima  13224  ghmnsgpreima  13225  ghmf1  13229  ghmf1o  13231  conjghm  13232  qusghm  13238  ablpncan3  13273  eqgabl  13284  rngpropd  13326  imasrng  13327  qusrng  13329  srglmhm  13364  srgrmhm  13365  ringpropd  13409  imasring  13431  qusring2  13433  opprrngbg  13445  dvdsrvald  13460  dvdsrd  13461  dvdsrex  13465  dvdsrtr  13468  unitpropdg  13515  rhmopp  13543  issubrng2  13574  subrngintm  13576  subsubrng  13578  subrgintm  13607  subsubrg  13609  aprap  13619  lmodprop2d  13681  rmodislmod  13684  lssvacl  13698  lssvsubcl  13699  lssvscl  13708  islss3  13712  lss1d  13716  rnglidlmcl  13813  2idlcpblrng  13855  crngridl  13861  mulgghm2  13923  mulgrhm  13924  iuncld  14092  ssnei2  14134  topssnei  14139  restopnb  14158  cnfval  14171  cnpfval  14172  iscnp4  14195  cnptopco  14199  cncnpi  14205  cncnp  14207  cnconst2  14210  cnrest2  14213  cnptoprest  14216  cnptoprest2  14217  cnpdis  14219  lmss  14223  lmtopcnp  14227  neitx  14245  txcnp  14248  txrest  14253  txdis1cn  14255  txlm  14256  cnmpt21  14268  imasnopn  14276  xmetres2  14356  blvalps  14365  blval  14366  elbl2ps  14369  elbl2  14370  blhalf  14385  blssexps  14406  blssex  14407  ssblex  14408  blin2  14409  bdmetval  14477  xmetxp  14484  xmettx  14487  metcnpi3  14494  txmetcnp  14495  addcncntoplem  14528  fsumcncntop  14533  elcncf2  14538  mulc1cncf  14553  cncfco  14555  cncfmet  14556  cncfmptc  14559  mulcncf  14568  dedekindeulemub  14573  dedekindeulemloc  14574  dedekindeulemlu  14576  dedekindeu  14578  dedekindicclemub  14582  dedekindicclemloc  14583  dedekindicclemlu  14585  dedekindicclemicc  14587  dedekindicc  14588  ivthinclemlopn  14591  ivthinclemuopn  14593  limcimo  14611  cnplimccntop  14616  limccnp2lem  14622  limccnp2cntop  14623  dvfvalap  14627  dveflem  14664  reeff1olem  14669  reeff1oleme  14670  eflt  14673  sin0pilem2  14680  pilem3  14681  ioocosf1o  14752  cxplt  14813  cxple  14814  cxplt3  14817  apcxp2  14835  rprelogbmul  14850  rprelogbdiv  14852  logbgt0b  14861  logbgcd1irrap  14865  lgsdir2lem5  14911  lgsdi  14916  lgsne0  14917  lgseisenlem2  14929  2sqlem6  14945  2sqlem8  14948  2sqlem9  14949  2sqlem10  14950  nnti  15223  pwtrufal  15226  pwf1oexmid  15228  sssneq  15230  qdencn  15254  cvgcmp2n  15260  trilpolemlt1  15268  trirec0  15271  redc0  15284  reap0  15285  cndcap  15286  nconstwlpolemgt0  15291  neap0mkv  15296  supfz  15298  inffz  15299