Theorem simprr 500

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 476	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  simp1rr  1012  simp2rr  1016  simp3rr  1020  disjiun  3862  reg2exmidlema  4378  reg3exmidlemwe  4422  fvmptt  5430  fcof1  5600  fliftfun  5613  isotr  5633  riotass2  5672  acexmidlemab  5684  ovmpt2df  5814  grprinvlem  5877  1stconst  6024  2ndconst  6025  cnvf1olem  6027  f1od2  6038  smoiso  6105  tfrcldm  6166  tfrcl  6167  swoer  6360  erinxp  6406  ecopovsymg  6431  th3qlem1  6434  f1imaen2g  6590  mapdom1g  6643  fict  6664  fidifsnen  6666  dif1enen  6676  fiunsnnn  6677  fisbth  6679  findcard2d  6687  findcard2sd  6688  diffifi  6690  ac6sfi  6694  fimax2gtri  6697  nnwetri  6706  unsnfi  6709  unsnfidcex  6710  unsnfidcel  6711  fisseneq  6722  ssfirab  6723  fidcenumlemrk  6743  fidcenumlemr  6744  sbthlemi6  6751  sbthlemi8  6753  isbth  6756  supmaxti  6779  infminti  6802  ordiso2  6808  eldju2ndl  6843  eldju2ndr  6844  ctmlemr  6870  fodjum  6889  fodju0  6890  exmidfodomrlemrALT  6926  dfplpq2  7010  dfmpq2  7011  mulpipqqs  7029  distrnqg  7043  enq0sym  7088  enq0tr  7090  distrnq0  7115  prarloclem3  7153  genplt2i  7166  addlocpr  7192  prmuloc  7222  distrlem1prl  7238  distrlem1pru  7239  ltexprlemopl  7257  ltexprlemopu  7259  ltexprlemfl  7265  ltexprlemrl  7266  ltexprlemfu  7267  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  ltaprg  7275  prplnqu  7276  addextpr  7277  recexprlemdisj  7286  recexprlemloc  7287  aptiprleml  7295  aptiprlemu  7296  ltmprr  7298  archpr  7299  cauappcvgprlemopl  7302  cauappcvgprlemopu  7304  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlem1  7315  cauappcvgprlemlim  7317  caucvgprlemnkj  7322  caucvgprlemopl  7325  caucvgprlemopu  7327  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprprlemnkltj  7345  caucvgprprlemnkeqj  7346  caucvgprprlemnjltk  7347  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemopu  7355  caucvgprprlemdisj  7358  caucvgprprlemloc  7359  caucvgprprlemaddq  7364  recexgt0sr  7416  mulgt0sr  7420  prsrriota  7430  addcnsr  7468  mulcnsr  7469  mulcnsrec  7477  axmulcom  7503  rereceu  7521  axarch  7523  axcaucvglemres  7531  lelttr  7670  ltletr  7671  addcan  7759  addcan2  7760  addsub4  7822  ltadd2  7994  le2add  8019  lt2add  8020  lt2sub  8035  le2sub  8036  eqord1  8058  rereim  8160  apreap  8161  apreim  8177  mulreim  8178  apcotr  8181  apadd1  8182  addext  8184  apneg  8185  mulext1  8186  mulext  8188  ltleap  8204  mulap0  8220  mulcanapd  8227  rec11ap  8274  rec11rap  8275  divdivdivap  8277  ddcanap  8290  divadddivap  8291  prodgt0gt0  8409  prodgt0  8410  prodge0  8412  lemulge11  8424  lt2mul2div  8437  ltrec  8441  lerec  8442  lerec2  8447  ledivp1  8461  mulle0r  8502  nn0ge0div  8932  suprzclex  8943  qapne  9223  xrlelttr  9372  xrltletr  9373  xrre3  9388  xrrege0  9391  xaddge0  9444  xle2add  9445  xlt2add  9446  fzass4  9625  fzrev  9647  elfz1b  9653  eluzgtdifelfzo  9757  fzocatel  9759  exbtwnzlemex  9810  rebtwn2z  9815  modqid  9905  modqcyc  9915  modqaddabs  9918  modqaddmod  9919  mulqaddmodid  9920  modqadd2mod  9930  modqltm1p1mod  9932  modqsubmod  9938  modqsubmodmod  9939  modaddmodup  9943  modqmulmod  9945  modqmulmodr  9946  modqaddmulmod  9947  modqsubdir  9949  frec2uzisod  9963  iseqovex  10011  seqf  10015  seq3shft2  10023  monoord  10026  iseqf1olemnab  10038  seq3distr  10063  expnegzap  10104  ltexp2a  10122  le2sq2  10145  bernneq  10189  expnlbnd2  10194  nn0opth2  10247  faclbnd  10264  bcval5  10286  hashcl  10304  hashen  10307  fihashdom  10326  hashunlem  10327  hashun  10328  hashxp  10349  fimaxq  10350  zfz1isolem1  10360  zfz1iso  10361  seq3coll  10362  cvg1nlemres  10533  cvg1n  10534  resqrexlemp1rp  10554  resqrexlemoverl  10569  resqrexlemex  10573  sqrtsq  10592  abslt  10636  absle  10637  abs3lem  10659  maxleastlt  10763  maxltsup  10766  fimaxre2  10773  negfi  10774  xrmaxleastlt  10799  xrmaxltsup  10801  xrmaxaddlem  10803  2clim  10844  climcn2  10852  addcn2  10853  mulcn2  10855  reccn2ap  10856  climge0  10868  climcau  10890  summodclem2  10925  summodc  10926  zsumdc  10927  fsumf1o  10933  fisumss  10935  fsum3cvg3  10939  fsumcl2lem  10941  fsumadd  10949  mptfzshft  10985  fsumrev  10986  fsummulc2  10991  fsumconst  10997  modfsummod  11001  fsumrelem  11014  binom  11027  cvgratnn  11074  mertenslemub  11077  efcllem  11098  tanaddaplem  11178  moddvds  11232  dvdsflip  11279  oexpneg  11304  nn0o  11334  fldivndvdslt  11362  zsupcllemstep  11368  zsupcllemex  11369  zssinfcl  11371  bezoutlemnewy  11412  bezoutlemstep  11413  bezoutlemeu  11423  dfgcd3  11426  dfgcd2  11430  dvdsmulgcd  11441  bezoutr  11448  lcmgcdlem  11486  coprmdvds2  11502  qredeu  11506  rpdvds  11508  cncongr1  11512  prmind2  11529  isprm6  11553  oddpwdclemdc  11578  nonsq  11612  hashdvds  11624  crth  11627  hashgcdlem  11630  hashgcdeq  11631  isstruct2r  11654  setscom  11683  iuncld  11967  ssnei2  12009  topssnei  12014  restopnb  12033  cnfval  12046  cnpfval  12047  iscnp4  12069  cnptopco  12073  cncnpi  12079  cncnp  12081  cnconst2  12084  cnrest2  12087  cnptoprest  12090  cnptoprest2  12091  cnpdis  12093  lmss  12097  lmtopcnp  12101  xmetres2  12165  blvalps  12174  blval  12175  elbl2ps  12178  elbl2  12179  blhalf  12194  blssexps  12215  blssex  12216  ssblex  12217  blin2  12218  bdmetval  12286  metcnpi3  12299  elcncf2  12327  mulc1cncf  12342  cncfco  12344  cncfmet  12345  cncfmptc  12346  mulcncf  12354  nnsucpred  12596  nnti  12597  qdencn  12620  supfz  12621  inffz  12622