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  990  simp1rr  1090  simp2rr  1094  simp3rr  1098  elpr2elpr  3882  invdisjrab  4105  disjiun  4106  reg2exmidlema  4658  reg3exmidlemwe  4703  nnsucpred  4741  iotam  5346  fvmptt  5771  fcof1  5958  fliftfun  5971  isotr  5991  riotass2  6034  acexmidlemab  6046  ovmpodf  6187  fnmpoovd  6413  1stconst  6419  2ndconst  6420  cnvf1olem  6422  f1od2  6433  suppcofn  6468  smoiso  6535  tfrcldm  6596  tfrcl  6597  nntr2  6738  swoer  6797  erinxp  6845  ecopovsymg  6870  th3qlem1  6873  f1imaen2g  7035  pw2f1odclem  7089  mapdom1g  7102  fict  7125  fidifsnen  7127  dif1enen  7139  fiunsnnn  7140  fisbth  7142  findcard2d  7150  findcard2sd  7151  diffifi  7153  ac6sfi  7157  fimax2gtri  7161  nnwetri  7178  unsnfi  7181  unsnfidcex  7182  unsnfidcel  7183  fisseneq  7197  ssfirab  7199  exmidssfi  7201  fidcenumlemrk  7226  fidcenumlemr  7227  sbthlemi6  7234  sbthlemi8  7236  isbth  7239  fiuni  7267  supmaxti  7297  infminti  7320  ordiso2  7328  eldju2ndl  7365  eldju2ndr  7366  omp1eomlem  7387  difinfsnlem  7392  difinfinf  7394  ctmlemr  7401  ctssdccl  7404  nninfninc  7416  fodjum  7439  fodju0  7440  omniwomnimkv  7460  exmidfodomrlemrALT  7508  acfun  7516  exmidaclem  7517  netap  7573  exmidmotap  7580  ccfunen  7583  cc1  7584  cc2lem  7585  dfplpq2  7674  dfmpq2  7675  mulpipqqs  7693  distrnqg  7707  enq0sym  7752  enq0tr  7754  distrnq0  7779  prarloclem3  7817  genplt2i  7830  addlocpr  7856  prmuloc  7886  distrlem1prl  7902  distrlem1pru  7903  ltexprlemopl  7921  ltexprlemopu  7923  ltexprlemfl  7929  ltexprlemrl  7930  ltexprlemfu  7931  ltexprlemru  7932  addcanprleml  7934  addcanprlemu  7935  ltaprg  7939  prplnqu  7940  addextpr  7941  recexprlemdisj  7950  recexprlemloc  7951  aptiprleml  7959  aptiprlemu  7960  ltmprr  7962  archpr  7963  cauappcvgprlemopl  7966  cauappcvgprlemopu  7968  cauappcvgprlemdisj  7971  cauappcvgprlemloc  7972  cauappcvgprlem1  7979  cauappcvgprlemlim  7981  caucvgprlemnkj  7986  caucvgprlemopl  7989  caucvgprlemopu  7991  caucvgprlemdisj  7994  caucvgprlemloc  7995  caucvgprprlemnkltj  8009  caucvgprprlemnkeqj  8010  caucvgprprlemnjltk  8011  caucvgprprlemml  8014  caucvgprprlemmu  8015  caucvgprprlemopl  8017  caucvgprprlemopu  8019  caucvgprprlemdisj  8022  caucvgprprlemloc  8023  caucvgprprlemaddq  8028  suplocexprlemrl  8037  suplocexprlemmu  8038  suplocexprlemru  8039  suplocexprlemdisj  8040  suplocexprlemloc  8041  suplocexprlemex  8042  suplocexprlemub  8043  recexgt0sr  8093  mulgt0sr  8098  prsrriota  8108  suplocsrlem  8128  addcnsr  8154  mulcnsr  8155  mulcnsrec  8163  axmulcom  8191  rereceu  8209  axarch  8211  axcaucvglemres  8219  axpre-suploclemres  8221  lelttr  8367  ltletr  8368  addcan  8458  addcan2  8459  addsub4  8521  ltadd2  8698  le2add  8723  lt2add  8724  lt2sub  8739  le2sub  8740  eqord1  8762  rereim  8865  apreap  8866  apreim  8882  mulreim  8883  apcotr  8886  apadd1  8887  addext  8889  apneg  8890  mulext1  8891  mulext  8893  ltleap  8911  aprcl  8925  mulap0  8933  mulcanapd  8940  recapb  8950  rec11ap  8989  rec11rap  8990  divdivdivap  8992  ddcanap  9005  divadddivap  9006  prodgt0gt0  9130  prodgt0  9131  prodge0  9133  lemulge11  9145  lt2mul2div  9158  ltrec  9162  lerec  9163  lerec2  9168  ledivp1  9182  mulle0r  9223  nn0ge0div  9671  suprzclex  9682  qapne  9977  xrlelttr  10145  xrltletr  10146  xrre3  10161  xrrege0  10164  xaddge0  10217  xle2add  10218  xlt2add  10219  fzass4  10402  fzrev  10425  elfz1b  10431  eluzgtdifelfzo  10549  fzocatel  10551  zsupcllemstep  10596  zsupcllemex  10597  zssinfcl  10599  suprzubdc  10603  exbtwnzlemex  10616  rebtwn2z  10621  modqid  10718  modqcyc  10728  modqaddabs  10731  modqaddmod  10732  mulqaddmodid  10733  modqadd2mod  10743  modqltm1p1mod  10745  modqsubmod  10751  modqsubmodmod  10752  modaddmodup  10756  modqmulmod  10758  modqmulmodr  10759  modqaddmulmod  10760  modqsubdir  10762  frec2uzisod  10776  uzennn  10805  iseqovex  10827  seqvalcd  10830  seq1g  10832  seqf  10833  seqovcd  10836  seqclg  10841  seqm1g  10843  seq3shft2  10850  seqshft2g  10851  monoord  10854  iseqf1olemnab  10870  seqf1oglem1  10888  seqf1og  10890  seqhomog  10899  seqfeq4g  10900  seq3distr  10901  expnegzap  10942  ltexp2a  10960  le2sq2  10984  bernneq  11030  expnlbnd2  11035  nn0ltexp2  11079  nn0opth2  11094  faclbnd  11111  bcval5  11133  hashcl  11152  hashen  11155  fihashdom  11175  hashunlem  11176  hashun  11177  hashxp  11199  hashmap  11200  fimaxq  11202  sseqn  11211  hashfibclem  11214  hashfibc  11215  zfz1isolem1  11220  zfz1iso  11221  seq3coll  11222  sswrd  11241  ccatw2s1p1g  11341  ccatw2s1p2  11342  ccat2s1fstg  11344  wrdind  11422  pfxccatin12lem1  11428  pfxccatin12lem3  11432  reuccatpfxs1lem  11446  cvg1nlemres  11678  cvg1n  11679  resqrexlemp1rp  11699  resqrexlemoverl  11714  resqrexlemex  11718  sqrtsq  11737  abslt  11781  absle  11782  abs3lem  11804  maxleastlt  11908  maxltsup  11911  fimaxre2  11920  negfi  11921  xrmaxleastlt  11949  xrmaxltsup  11951  xrmaxaddlem  11953  2clim  11994  climcn2  12002  addcn2  12003  mulcn2  12005  reccn2ap  12006  climge0  12018  climcau  12040  fzf1o  12069  summodclem2  12076  summodc  12077  zsumdc  12078  fsumf1o  12084  fisumss  12086  fsum3cvg3  12090  fsumcl2lem  12092  fsumadd  12100  mptfzshft  12136  fsumrev  12137  fsummulc2  12142  fsumconst  12148  modfsummod  12152  fsumrelem  12165  binom  12178  cvgratnn  12225  mertenslemub  12228  prodmodclem2  12271  prodmodc  12272  zproddc  12273  fprodf1o  12282  fprodssdc  12284  fprodmul  12285  fprodcl2lem  12299  fprodrev  12313  fprodconst  12314  fprodap0  12315  fprodrec  12323  fprodap0f  12330  fprodle  12334  fprodmodd  12335  efcllem  12353  tanaddaplem  12432  moddvds  12493  dvdsflip  12545  oexpneg  12571  nn0o  12601  fldivndvdslt  12631  bitsfi  12651  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlemeu  12711  dfgcd3  12714  dfgcd2  12718  dvdsmulgcd  12729  bezoutr  12736  nninfctlemfo  12744  lcmgcdlem  12782  coprmdvds2  12798  qredeu  12802  rpdvds  12804  cncongr1  12808  prmind2  12825  isprm5lem  12846  isprm6  12852  oddpwdclemdc  12878  nonsq  12912  hashdvds  12926  crth  12929  eulerthlemh  12936  prmdiveq  12941  hashgcdlem  12943  hashgcdeq  12945  nnnn0modprm0  12961  pclemub  12993  pceu  13001  pcmul  13007  pcqmul  13009  pcgcd1  13034  pc2dvds  13036  difsqpwdvds  13044  pcmpt  13049  prmpwdvds  13061  1arith  13073  mul4sq  13100  4sqlemafi  13101  4sqlemffi  13102  4sqexercise2  13105  ballotfilemfc0  13157  ballotfilemfcc  13158  ennnfonelemg  13175  ennnfonelemex  13186  ennnfonelemrnh  13188  ennnfonelemf1  13190  ennnfonelemrn  13191  ennnfonelemdm  13192  ennnfonelemim  13196  ennnfone  13197  ctinf  13202  ctiunctlemfo  13211  nninfdclemcl  13220  nninfdclemf  13221  nninfdclemp1  13222  unbendc  13226  isstruct2r  13244  setscom  13273  ercpbl  13565  opifismgmdc  13605  grpinvalem  13619  igsumvalx  13623  gsumfzval  13625  gsumval2  13631  sgrppropd  13647  prdssgrpd  13649  mndpropd  13674  issubmnd  13676  submnd0  13678  prdsmndd  13682  mhmf1o  13704  subsubm  13717  0mhm  13720  resmhm  13721  mhmco  13724  mhmima  13725  mhmeql  13726  gsumfzz  13729  gsumwsubmcl  13730  gsumfzcl  13733  grprcan  13771  grpinvid1  13786  grpinvid2  13787  grplcan  13796  grplmulf1o  13808  grpnpncan0  13830  dfgrp3mlem  13832  grplactcnv  13836  pwssub  13847  mulgval  13860  mulgfng  13862  mulgnngsum  13865  mulg1  13867  mulgnnp1  13868  mulgneg  13878  mulgnndir  13889  mulgdirlem  13891  mulgnn0ass  13896  mulgass  13897  subgmulg  13926  issubg4m  13931  subsubg  13935  subgintm  13936  isnsg3  13945  eqgcpbl  13966  ghmeql  14005  ghmnsgima  14006  ghmnsgpreima  14007  ghmf1  14011  ghmf1o  14013  conjghm  14014  qusghm  14020  ablpncan3  14055  invghm  14067  eqgabl  14068  gsumfzreidx  14075  gsumfzsubmcl  14076  gsumfzmptfidmadd  14077  gsumfzmhm  14081  rngpropd  14120  imasrng  14121  qusrng  14123  srglmhm  14158  srgrmhm  14159  ringpropd  14203  ringlghm  14226  ringrghm  14227  imasring  14229  qusring2  14231  opprrngbg  14243  dvdsrvald  14260  dvdsrd  14261  dvdsrex  14265  dvdsrtr  14268  unitpropdg  14315  rhmopp  14343  isnzr2  14351  issubrng2  14378  subrngintm  14380  subsubrng  14382  subrgintm  14411  subsubrg  14413  rhmpropd  14422  ringunitap  14453  aprap  14458  drngunitap  14468  lmodprop2d  14545  rmodislmod  14548  lssvacl  14562  lssvsubcl  14563  lssvscl  14572  islss3  14576  lss1d  14580  rnglidlmcl  14677  2idlcpblrng  14720  crngridl  14727  expghmap  14804  mulgghm2  14805  mulgrhm  14806  znf1o  14848  znleval  14850  znidom  14854  znidomb  14855  znunit  14856  psrbagcon  14875  mplsubgfilemcl  14903  iuncld  15029  ssnei2  15071  topssnei  15076  restopnb  15095  cnfval  15108  cnpfval  15109  iscnp4  15132  cnptopco  15136  cncnpi  15142  cncnp  15144  cnconst2  15147  cnrest2  15150  cnptoprest  15153  cnptoprest2  15154  cnpdis  15156  lmss  15160  lmtopcnp  15164  neitx  15182  txcnp  15185  txrest  15190  txdis1cn  15192  txlm  15193  cnmpt21  15205  imasnopn  15213  xmetres2  15293  blvalps  15302  blval  15303  elbl2ps  15306  elbl2  15307  blhalf  15322  blssexps  15343  blssex  15344  ssblex  15345  blin2  15346  bdmetval  15414  xmetxp  15421  xmettx  15424  metcnpi3  15431  txmetcnp  15432  addcncntoplem  15475  fsumcncntop  15481  elcncf2  15488  mulc1cncf  15503  cncfco  15505  cncfmet  15506  cncfmptc  15510  mulcncf  15522  dedekindeulemub  15532  dedekindeulemloc  15533  dedekindeulemlu  15535  dedekindeu  15537  dedekindicclemub  15541  dedekindicclemloc  15542  dedekindicclemlu  15544  dedekindicclemicc  15546  dedekindicc  15547  ivthinclemlopn  15550  ivthinclemuopn  15552  dich0  15566  limcimo  15579  cnplimccntop  15584  limccnp2lem  15590  limccnp2cntop  15591  dvfvalap  15595  dveflem  15640  plycolemc  15672  plyco  15673  plyrecj  15677  reeff1olem  15685  reeff1oleme  15686  eflt  15689  sin0pilem2  15696  pilem3  15697  ioocosf1o  15768  cxplt  15830  cxple  15831  cxplt3  15834  apcxp2  15853  rprelogbmul  15869  rprelogbdiv  15871  logbgt0b  15880  logbgcd1irrap  15884  pellexlem3  15896  mpodvdsmulf1o  15907  fsumdvdsmul  15908  lgsdir2lem5  15954  lgsdi  15959  lgsne0  15960  gausslemma2dlem1f1o  15982  lgseisenlem2  15993  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad2lem2  16004  lgsquad2  16005  2sqlem6  16042  2sqlem8  16045  2sqlem9  16046  2sqlem10  16047  upgredg  16188  usgredg4  16259  uspgredg2vlem  16264  usgr1eop  16289  upgrspanop  16327  umgrspanop  16328  usgrspanop  16329  vtxedgfi  16333  vtxlpfi  16334  iswlkg  16373  upgriswlkdc  16404  upgr2wlkdc  16421  clwwlkccatlem  16444  clwwlknonex2e  16484  nnti  16815  pwtrufal  16820  pwf1oexmid  16822  sssneq  16825  qdencn  16856  cvgcmp2n  16866  trilpolemlt1  16874  trirec0  16877  qdiff  16882  redc0  16891  reap0  16892  cndcap  16893  nconstwlpolemgt0  16899  neap0mkv  16904  supfz  16906  inffz  16907  gfsumval  16911  gfsumz  16918  gfsumcl  16919