Theorem simprr 522

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  simp1rr  1048  simp2rr  1052  simp3rr  1056  disjiun  3932  reg2exmidlema  4457  reg3exmidlemwe  4501  nnsucpred  4538  fvmptt  5520  fcof1  5692  fliftfun  5705  isotr  5725  riotass2  5764  acexmidlemab  5776  ovmpodf  5910  grprinvlem  5973  fnmpoovd  6120  1stconst  6126  2ndconst  6127  cnvf1olem  6129  f1od2  6140  smoiso  6207  tfrcldm  6268  tfrcl  6269  nntr2  6407  swoer  6465  erinxp  6511  ecopovsymg  6536  th3qlem1  6539  f1imaen2g  6695  mapdom1g  6749  fict  6770  fidifsnen  6772  dif1enen  6782  fiunsnnn  6783  fisbth  6785  findcard2d  6793  findcard2sd  6794  diffifi  6796  ac6sfi  6800  fimax2gtri  6803  nnwetri  6812  unsnfi  6815  unsnfidcex  6816  unsnfidcel  6817  fisseneq  6828  ssfirab  6830  fidcenumlemrk  6850  fidcenumlemr  6851  sbthlemi6  6858  sbthlemi8  6860  isbth  6863  fiuni  6874  supmaxti  6899  infminti  6922  ordiso2  6928  eldju2ndl  6965  eldju2ndr  6966  omp1eomlem  6987  difinfsnlem  6992  difinfinf  6994  ctmlemr  7001  ctssdccl  7004  fodjum  7026  fodju0  7027  omniwomnimkv  7049  exmidfodomrlemrALT  7076  acfun  7080  exmidaclem  7081  ccfunen  7096  cc1  7097  cc2lem  7098  dfplpq2  7186  dfmpq2  7187  mulpipqqs  7205  distrnqg  7219  enq0sym  7264  enq0tr  7266  distrnq0  7291  prarloclem3  7329  genplt2i  7342  addlocpr  7368  prmuloc  7398  distrlem1prl  7414  distrlem1pru  7415  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  ltaprg  7451  prplnqu  7452  addextpr  7453  recexprlemdisj  7462  recexprlemloc  7463  aptiprleml  7471  aptiprlemu  7472  ltmprr  7474  archpr  7475  cauappcvgprlemopl  7478  cauappcvgprlemopu  7480  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlem1  7491  cauappcvgprlemlim  7493  caucvgprlemnkj  7498  caucvgprlemopl  7501  caucvgprlemopu  7503  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnjltk  7523  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemopu  7531  caucvgprprlemdisj  7534  caucvgprprlemloc  7535  caucvgprprlemaddq  7540  suplocexprlemrl  7549  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemex  7554  suplocexprlemub  7555  recexgt0sr  7605  mulgt0sr  7610  prsrriota  7620  suplocsrlem  7640  addcnsr  7666  mulcnsr  7667  mulcnsrec  7675  axmulcom  7703  rereceu  7721  axarch  7723  axcaucvglemres  7731  axpre-suploclemres  7733  lelttr  7876  ltletr  7877  addcan  7966  addcan2  7967  addsub4  8029  ltadd2  8205  le2add  8230  lt2add  8231  lt2sub  8246  le2sub  8247  eqord1  8269  rereim  8372  apreap  8373  apreim  8389  mulreim  8390  apcotr  8393  apadd1  8394  addext  8396  apneg  8397  mulext1  8398  mulext  8400  ltleap  8418  aprcl  8432  mulap0  8439  mulcanapd  8446  rec11ap  8494  rec11rap  8495  divdivdivap  8497  ddcanap  8510  divadddivap  8511  prodgt0gt0  8633  prodgt0  8634  prodge0  8636  lemulge11  8648  lt2mul2div  8661  ltrec  8665  lerec  8666  lerec2  8671  ledivp1  8685  mulle0r  8726  nn0ge0div  9162  suprzclex  9173  qapne  9458  xrlelttr  9619  xrltletr  9620  xrre3  9635  xrrege0  9638  xaddge0  9691  xle2add  9692  xlt2add  9693  fzass4  9873  fzrev  9895  elfz1b  9901  eluzgtdifelfzo  10005  fzocatel  10007  exbtwnzlemex  10058  rebtwn2z  10063  modqid  10153  modqcyc  10163  modqaddabs  10166  modqaddmod  10167  mulqaddmodid  10168  modqadd2mod  10178  modqltm1p1mod  10180  modqsubmod  10186  modqsubmodmod  10187  modaddmodup  10191  modqmulmod  10193  modqmulmodr  10194  modqaddmulmod  10195  modqsubdir  10197  frec2uzisod  10211  uzennn  10240  iseqovex  10260  seqvalcd  10263  seqf  10265  seqovcd  10267  seq3shft2  10277  monoord  10280  iseqf1olemnab  10292  seq3distr  10317  expnegzap  10358  ltexp2a  10376  le2sq2  10399  bernneq  10443  expnlbnd2  10448  nn0opth2  10502  faclbnd  10519  bcval5  10541  hashcl  10559  hashen  10562  fihashdom  10581  hashunlem  10582  hashun  10583  hashxp  10604  fimaxq  10605  zfz1isolem1  10615  zfz1iso  10616  seq3coll  10617  cvg1nlemres  10789  cvg1n  10790  resqrexlemp1rp  10810  resqrexlemoverl  10825  resqrexlemex  10829  sqrtsq  10848  abslt  10892  absle  10893  abs3lem  10915  maxleastlt  11019  maxltsup  11022  fimaxre2  11030  negfi  11031  xrmaxleastlt  11057  xrmaxltsup  11059  xrmaxaddlem  11061  2clim  11102  climcn2  11110  addcn2  11111  mulcn2  11113  reccn2ap  11114  climge0  11126  climcau  11148  summodclem2  11183  summodc  11184  zsumdc  11185  fsumf1o  11191  fisumss  11193  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  mptfzshft  11243  fsumrev  11244  fsummulc2  11249  fsumconst  11255  modfsummod  11259  fsumrelem  11272  binom  11285  cvgratnn  11332  mertenslemub  11335  prodmodclem2  11378  prodmodc  11379  zproddc  11380  efcllem  11402  tanaddaplem  11481  moddvds  11538  dvdsflip  11585  oexpneg  11610  nn0o  11640  fldivndvdslt  11668  zsupcllemstep  11674  zsupcllemex  11675  zssinfcl  11677  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemeu  11731  dfgcd3  11734  dfgcd2  11738  dvdsmulgcd  11749  bezoutr  11756  lcmgcdlem  11794  coprmdvds2  11810  qredeu  11814  rpdvds  11816  cncongr1  11820  prmind2  11837  isprm6  11861  oddpwdclemdc  11887  nonsq  11921  hashdvds  11933  crth  11936  hashgcdlem  11939  hashgcdeq  11940  ennnfonelemg  11952  ennnfonelemex  11963  ennnfonelemrnh  11965  ennnfonelemf1  11967  ennnfonelemrn  11968  ennnfonelemdm  11969  ennnfonelemim  11973  ennnfone  11974  ctinf  11979  ctiunctlemfo  11988  isstruct2r  12009  setscom  12038  iuncld  12323  ssnei2  12365  topssnei  12370  restopnb  12389  cnfval  12402  cnpfval  12403  iscnp4  12426  cnptopco  12430  cncnpi  12436  cncnp  12438  cnconst2  12441  cnrest2  12444  cnptoprest  12447  cnptoprest2  12448  cnpdis  12450  lmss  12454  lmtopcnp  12458  neitx  12476  txcnp  12479  txrest  12484  txdis1cn  12486  txlm  12487  cnmpt21  12499  imasnopn  12507  xmetres2  12587  blvalps  12596  blval  12597  elbl2ps  12600  elbl2  12601  blhalf  12616  blssexps  12637  blssex  12638  ssblex  12639  blin2  12640  bdmetval  12708  xmetxp  12715  xmettx  12718  metcnpi3  12725  txmetcnp  12726  addcncntoplem  12759  fsumcncntop  12764  elcncf2  12769  mulc1cncf  12784  cncfco  12786  cncfmet  12787  cncfmptc  12790  mulcncf  12799  dedekindeulemub  12804  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeu  12809  dedekindicclemub  12813  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemicc  12818  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemuopn  12824  limcimo  12842  cnplimccntop  12847  limccnp2lem  12853  limccnp2cntop  12854  dvfvalap  12858  dveflem  12895  reeff1olem  12900  reeff1oleme  12901  eflt  12904  sin0pilem2  12911  pilem3  12912  ioocosf1o  12983  cxplt  13044  cxple  13045  cxplt3  13048  apcxp2  13066  rprelogbmul  13080  rprelogbdiv  13082  logbgt0b  13091  logbgcd1irrap  13095  nnti  13362  pwtrufal  13365  pwf1oexmid  13367  sssneq  13370  qdencn  13397  cvgcmp2n  13403  trilpolemlt1  13409  trirec0  13412  supfz  13428  inffz  13429