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:  dfifp2dc  987  simp1rr  1087  simp2rr  1091  simp3rr  1095  elpr2elpr  3857  invdisjrab  4080  disjiun  4081  reg2exmidlema  4630  reg3exmidlemwe  4675  nnsucpred  4713  iotam  5316  fvmptt  5734  fcof1  5919  fliftfun  5932  isotr  5952  riotass2  5995  acexmidlemab  6007  ovmpodf  6148  fnmpoovd  6375  1stconst  6381  2ndconst  6382  cnvf1olem  6384  f1od2  6395  smoiso  6463  tfrcldm  6524  tfrcl  6525  nntr2  6666  swoer  6725  erinxp  6773  ecopovsymg  6798  th3qlem1  6801  f1imaen2g  6962  pw2f1odclem  7015  mapdom1g  7028  fict  7050  fidifsnen  7052  dif1enen  7064  fiunsnnn  7065  fisbth  7067  findcard2d  7075  findcard2sd  7076  diffifi  7078  ac6sfi  7082  fimax2gtri  7086  nnwetri  7103  unsnfi  7106  unsnfidcex  7107  unsnfidcel  7108  fisseneq  7121  ssfirab  7123  exmidssfi  7125  fidcenumlemrk  7147  fidcenumlemr  7148  sbthlemi6  7155  sbthlemi8  7157  isbth  7160  fiuni  7171  supmaxti  7197  infminti  7220  ordiso2  7228  eldju2ndl  7265  eldju2ndr  7266  omp1eomlem  7287  difinfsnlem  7292  difinfinf  7294  ctmlemr  7301  ctssdccl  7304  nninfninc  7316  fodjum  7339  fodju0  7340  omniwomnimkv  7360  exmidfodomrlemrALT  7407  acfun  7415  exmidaclem  7416  netap  7466  exmidmotap  7473  ccfunen  7476  cc1  7477  cc2lem  7478  dfplpq2  7567  dfmpq2  7568  mulpipqqs  7586  distrnqg  7600  enq0sym  7645  enq0tr  7647  distrnq0  7672  prarloclem3  7710  genplt2i  7723  addlocpr  7749  prmuloc  7779  distrlem1prl  7795  distrlem1pru  7796  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  ltaprg  7832  prplnqu  7833  addextpr  7834  recexprlemdisj  7843  recexprlemloc  7844  aptiprleml  7852  aptiprlemu  7853  ltmprr  7855  archpr  7856  cauappcvgprlemopl  7859  cauappcvgprlemopu  7861  cauappcvgprlemdisj  7864  cauappcvgprlemloc  7865  cauappcvgprlem1  7872  cauappcvgprlemlim  7874  caucvgprlemnkj  7879  caucvgprlemopl  7882  caucvgprlemopu  7884  caucvgprlemdisj  7887  caucvgprlemloc  7888  caucvgprprlemnkltj  7902  caucvgprprlemnkeqj  7903  caucvgprprlemnjltk  7904  caucvgprprlemml  7907  caucvgprprlemmu  7908  caucvgprprlemopl  7910  caucvgprprlemopu  7912  caucvgprprlemdisj  7915  caucvgprprlemloc  7916  caucvgprprlemaddq  7921  suplocexprlemrl  7930  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemex  7935  suplocexprlemub  7936  recexgt0sr  7986  mulgt0sr  7991  prsrriota  8001  suplocsrlem  8021  addcnsr  8047  mulcnsr  8048  mulcnsrec  8056  axmulcom  8084  rereceu  8102  axarch  8104  axcaucvglemres  8112  axpre-suploclemres  8114  lelttr  8261  ltletr  8262  addcan  8352  addcan2  8353  addsub4  8415  ltadd2  8592  le2add  8617  lt2add  8618  lt2sub  8633  le2sub  8634  eqord1  8656  rereim  8759  apreap  8760  apreim  8776  mulreim  8777  apcotr  8780  apadd1  8781  addext  8783  apneg  8784  mulext1  8785  mulext  8787  ltleap  8805  aprcl  8819  mulap0  8827  mulcanapd  8834  recapb  8844  rec11ap  8883  rec11rap  8884  divdivdivap  8886  ddcanap  8899  divadddivap  8900  prodgt0gt0  9024  prodgt0  9025  prodge0  9027  lemulge11  9039  lt2mul2div  9052  ltrec  9056  lerec  9057  lerec2  9062  ledivp1  9076  mulle0r  9117  nn0ge0div  9560  suprzclex  9571  qapne  9866  xrlelttr  10034  xrltletr  10035  xrre3  10050  xrrege0  10053  xaddge0  10106  xle2add  10107  xlt2add  10108  fzass4  10290  fzrev  10312  elfz1b  10318  eluzgtdifelfzo  10435  fzocatel  10437  zsupcllemstep  10482  zsupcllemex  10483  zssinfcl  10485  suprzubdc  10489  exbtwnzlemex  10502  rebtwn2z  10507  modqid  10604  modqcyc  10614  modqaddabs  10617  modqaddmod  10618  mulqaddmodid  10619  modqadd2mod  10629  modqltm1p1mod  10631  modqsubmod  10637  modqsubmodmod  10638  modaddmodup  10642  modqmulmod  10644  modqmulmodr  10645  modqaddmulmod  10646  modqsubdir  10648  frec2uzisod  10662  uzennn  10691  iseqovex  10713  seqvalcd  10716  seq1g  10718  seqf  10719  seqovcd  10722  seqclg  10727  seqm1g  10729  seq3shft2  10736  seqshft2g  10737  monoord  10740  iseqf1olemnab  10756  seqf1oglem1  10774  seqf1og  10776  seqhomog  10785  seqfeq4g  10786  seq3distr  10787  expnegzap  10828  ltexp2a  10846  le2sq2  10870  bernneq  10915  expnlbnd2  10920  nn0ltexp2  10964  nn0opth2  10979  faclbnd  10996  bcval5  11018  hashcl  11036  hashen  11039  fihashdom  11059  hashunlem  11060  hashun  11061  hashxp  11083  fimaxq  11084  zfz1isolem1  11097  zfz1iso  11098  seq3coll  11099  sswrd  11115  ccatw2s1p1g  11215  ccatw2s1p2  11216  ccat2s1fstg  11218  wrdind  11296  pfxccatin12lem1  11302  pfxccatin12lem3  11306  reuccatpfxs1lem  11320  cvg1nlemres  11539  cvg1n  11540  resqrexlemp1rp  11560  resqrexlemoverl  11575  resqrexlemex  11579  sqrtsq  11598  abslt  11642  absle  11643  abs3lem  11665  maxleastlt  11769  maxltsup  11772  fimaxre2  11781  negfi  11782  xrmaxleastlt  11810  xrmaxltsup  11812  xrmaxaddlem  11814  2clim  11855  climcn2  11863  addcn2  11864  mulcn2  11866  reccn2ap  11867  climge0  11879  climcau  11901  summodclem2  11936  summodc  11937  zsumdc  11938  fsumf1o  11944  fisumss  11946  fsum3cvg3  11950  fsumcl2lem  11952  fsumadd  11960  mptfzshft  11996  fsumrev  11997  fsummulc2  12002  fsumconst  12008  modfsummod  12012  fsumrelem  12025  binom  12038  cvgratnn  12085  mertenslemub  12088  prodmodclem2  12131  prodmodc  12132  zproddc  12133  fprodf1o  12142  fprodssdc  12144  fprodmul  12145  fprodcl2lem  12159  fprodrev  12173  fprodconst  12174  fprodap0  12175  fprodrec  12183  fprodap0f  12190  fprodle  12194  fprodmodd  12195  efcllem  12213  tanaddaplem  12292  moddvds  12353  dvdsflip  12405  oexpneg  12431  nn0o  12461  fldivndvdslt  12491  bitsfi  12511  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemeu  12571  dfgcd3  12574  dfgcd2  12578  dvdsmulgcd  12589  bezoutr  12596  nninfctlemfo  12604  lcmgcdlem  12642  coprmdvds2  12658  qredeu  12662  rpdvds  12664  cncongr1  12668  prmind2  12685  isprm5lem  12706  isprm6  12712  oddpwdclemdc  12738  nonsq  12772  hashdvds  12786  crth  12789  eulerthlemh  12796  prmdiveq  12801  hashgcdlem  12803  hashgcdeq  12805  nnnn0modprm0  12821  pclemub  12853  pceu  12861  pcmul  12867  pcqmul  12869  pcgcd1  12894  pc2dvds  12896  difsqpwdvds  12904  pcmpt  12909  prmpwdvds  12921  1arith  12933  mul4sq  12960  4sqlemafi  12961  4sqlemffi  12962  4sqexercise2  12965  ennnfonelemg  13017  ennnfonelemex  13028  ennnfonelemrnh  13030  ennnfonelemf1  13032  ennnfonelemrn  13033  ennnfonelemdm  13034  ennnfonelemim  13038  ennnfone  13039  ctinf  13044  ctiunctlemfo  13053  nninfdclemcl  13062  nninfdclemf  13063  nninfdclemp1  13064  unbendc  13068  isstruct2r  13086  setscom  13115  ercpbl  13407  opifismgmdc  13447  grpinvalem  13461  igsumvalx  13465  gsumfzval  13467  gsumval2  13473  sgrppropd  13489  prdssgrpd  13491  mndpropd  13516  issubmnd  13518  submnd0  13520  prdsmndd  13524  mhmf1o  13546  subsubm  13559  0mhm  13562  resmhm  13563  mhmco  13566  mhmima  13567  mhmeql  13568  gsumfzz  13571  gsumwsubmcl  13572  gsumfzcl  13575  grprcan  13613  grpinvid1  13628  grpinvid2  13629  grplcan  13638  grplmulf1o  13650  grpnpncan0  13672  dfgrp3mlem  13674  grplactcnv  13678  pwssub  13689  mulgval  13702  mulgfng  13704  mulgnngsum  13707  mulg1  13709  mulgnnp1  13710  mulgneg  13720  mulgnndir  13731  mulgdirlem  13733  mulgnn0ass  13738  mulgass  13739  subgmulg  13768  issubg4m  13773  subsubg  13777  subgintm  13778  isnsg3  13787  eqgcpbl  13808  ghmeql  13847  ghmnsgima  13848  ghmnsgpreima  13849  ghmf1  13853  ghmf1o  13855  conjghm  13856  qusghm  13862  ablpncan3  13897  invghm  13909  eqgabl  13910  gsumfzreidx  13917  gsumfzsubmcl  13918  gsumfzmptfidmadd  13919  gsumfzmhm  13923  rngpropd  13961  imasrng  13962  qusrng  13964  srglmhm  13999  srgrmhm  14000  ringpropd  14044  ringlghm  14067  ringrghm  14068  imasring  14070  qusring2  14072  opprrngbg  14084  dvdsrvald  14100  dvdsrd  14101  dvdsrex  14105  dvdsrtr  14108  unitpropdg  14155  rhmopp  14183  isnzr2  14191  issubrng2  14217  subrngintm  14219  subsubrng  14221  subrgintm  14250  subsubrg  14252  rhmpropd  14261  aprap  14293  lmodprop2d  14355  rmodislmod  14358  lssvacl  14372  lssvsubcl  14373  lssvscl  14382  islss3  14386  lss1d  14390  rnglidlmcl  14487  2idlcpblrng  14530  crngridl  14537  expghmap  14614  mulgghm2  14615  mulgrhm  14616  znf1o  14658  znleval  14660  znidom  14664  znidomb  14665  znunit  14666  mplsubgfilemcl  14706  iuncld  14832  ssnei2  14874  topssnei  14879  restopnb  14898  cnfval  14911  cnpfval  14912  iscnp4  14935  cnptopco  14939  cncnpi  14945  cncnp  14947  cnconst2  14950  cnrest2  14953  cnptoprest  14956  cnptoprest2  14957  cnpdis  14959  lmss  14963  lmtopcnp  14967  neitx  14985  txcnp  14988  txrest  14993  txdis1cn  14995  txlm  14996  cnmpt21  15008  imasnopn  15016  xmetres2  15096  blvalps  15105  blval  15106  elbl2ps  15109  elbl2  15110  blhalf  15125  blssexps  15146  blssex  15147  ssblex  15148  blin2  15149  bdmetval  15217  xmetxp  15224  xmettx  15227  metcnpi3  15234  txmetcnp  15235  addcncntoplem  15278  fsumcncntop  15284  elcncf2  15291  mulc1cncf  15306  cncfco  15308  cncfmet  15309  cncfmptc  15313  mulcncf  15325  dedekindeulemub  15335  dedekindeulemloc  15336  dedekindeulemlu  15338  dedekindeu  15340  dedekindicclemub  15344  dedekindicclemloc  15345  dedekindicclemlu  15347  dedekindicclemicc  15349  dedekindicc  15350  ivthinclemlopn  15353  ivthinclemuopn  15355  dich0  15369  limcimo  15382  cnplimccntop  15387  limccnp2lem  15393  limccnp2cntop  15394  dvfvalap  15398  dveflem  15443  plycolemc  15475  plyco  15476  plyrecj  15480  reeff1olem  15488  reeff1oleme  15489  eflt  15492  sin0pilem2  15499  pilem3  15500  ioocosf1o  15571  cxplt  15633  cxple  15634  cxplt3  15637  apcxp2  15656  rprelogbmul  15672  rprelogbdiv  15674  logbgt0b  15683  logbgcd1irrap  15687  mpodvdsmulf1o  15707  fsumdvdsmul  15708  lgsdir2lem5  15754  lgsdi  15759  lgsne0  15760  gausslemma2dlem1f1o  15782  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2lem2  15804  lgsquad2  15805  2sqlem6  15842  2sqlem8  15845  2sqlem9  15846  2sqlem10  15847  upgredg  15988  usgredg4  16059  uspgredg2vlem  16064  usgr1eop  16089  vtxedgfi  16100  vtxlpfi  16101  iswlkg  16140  upgriswlkdc  16171  upgr2wlkdc  16186  clwwlkccatlem  16209  clwwlknonex2e  16249  nnti  16541  pwtrufal  16548  pwf1oexmid  16550  sssneq  16553  qdencn  16581  cvgcmp2n  16587  trilpolemlt1  16595  trirec0  16598  redc0  16611  reap0  16612  cndcap  16613  nconstwlpolemgt0  16618  neap0mkv  16623  supfz  16625  inffz  16626  gfsumval  16630