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  3854  invdisjrab  4077  disjiun  4078  reg2exmidlema  4626  reg3exmidlemwe  4671  nnsucpred  4709  iotam  5310  fvmptt  5728  fcof1  5913  fliftfun  5926  isotr  5946  riotass2  5989  acexmidlemab  6001  ovmpodf  6142  fnmpoovd  6367  1stconst  6373  2ndconst  6374  cnvf1olem  6376  f1od2  6387  smoiso  6454  tfrcldm  6515  tfrcl  6516  nntr2  6657  swoer  6716  erinxp  6764  ecopovsymg  6789  th3qlem1  6792  f1imaen2g  6953  pw2f1odclem  7003  mapdom1g  7016  fict  7038  fidifsnen  7040  dif1enen  7050  fiunsnnn  7051  fisbth  7053  findcard2d  7061  findcard2sd  7062  diffifi  7064  ac6sfi  7068  fimax2gtri  7071  nnwetri  7086  unsnfi  7089  unsnfidcex  7090  unsnfidcel  7091  fisseneq  7104  ssfirab  7106  fidcenumlemrk  7129  fidcenumlemr  7130  sbthlemi6  7137  sbthlemi8  7139  isbth  7142  fiuni  7153  supmaxti  7179  infminti  7202  ordiso2  7210  eldju2ndl  7247  eldju2ndr  7248  omp1eomlem  7269  difinfsnlem  7274  difinfinf  7276  ctmlemr  7283  ctssdccl  7286  nninfninc  7298  fodjum  7321  fodju0  7322  omniwomnimkv  7342  exmidfodomrlemrALT  7389  acfun  7397  exmidaclem  7398  netap  7448  exmidmotap  7455  ccfunen  7458  cc1  7459  cc2lem  7460  dfplpq2  7549  dfmpq2  7550  mulpipqqs  7568  distrnqg  7582  enq0sym  7627  enq0tr  7629  distrnq0  7654  prarloclem3  7692  genplt2i  7705  addlocpr  7731  prmuloc  7761  distrlem1prl  7777  distrlem1pru  7778  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemfl  7804  ltexprlemrl  7805  ltexprlemfu  7806  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  ltaprg  7814  prplnqu  7815  addextpr  7816  recexprlemdisj  7825  recexprlemloc  7826  aptiprleml  7834  aptiprlemu  7835  ltmprr  7837  archpr  7838  cauappcvgprlemopl  7841  cauappcvgprlemopu  7843  cauappcvgprlemdisj  7846  cauappcvgprlemloc  7847  cauappcvgprlem1  7854  cauappcvgprlemlim  7856  caucvgprlemnkj  7861  caucvgprlemopl  7864  caucvgprlemopu  7866  caucvgprlemdisj  7869  caucvgprlemloc  7870  caucvgprprlemnkltj  7884  caucvgprprlemnkeqj  7885  caucvgprprlemnjltk  7886  caucvgprprlemml  7889  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemopu  7894  caucvgprprlemdisj  7897  caucvgprprlemloc  7898  caucvgprprlemaddq  7903  suplocexprlemrl  7912  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemex  7917  suplocexprlemub  7918  recexgt0sr  7968  mulgt0sr  7973  prsrriota  7983  suplocsrlem  8003  addcnsr  8029  mulcnsr  8030  mulcnsrec  8038  axmulcom  8066  rereceu  8084  axarch  8086  axcaucvglemres  8094  axpre-suploclemres  8096  lelttr  8243  ltletr  8244  addcan  8334  addcan2  8335  addsub4  8397  ltadd2  8574  le2add  8599  lt2add  8600  lt2sub  8615  le2sub  8616  eqord1  8638  rereim  8741  apreap  8742  apreim  8758  mulreim  8759  apcotr  8762  apadd1  8763  addext  8765  apneg  8766  mulext1  8767  mulext  8769  ltleap  8787  aprcl  8801  mulap0  8809  mulcanapd  8816  recapb  8826  rec11ap  8865  rec11rap  8866  divdivdivap  8868  ddcanap  8881  divadddivap  8882  prodgt0gt0  9006  prodgt0  9007  prodge0  9009  lemulge11  9021  lt2mul2div  9034  ltrec  9038  lerec  9039  lerec2  9044  ledivp1  9058  mulle0r  9099  nn0ge0div  9542  suprzclex  9553  qapne  9842  xrlelttr  10010  xrltletr  10011  xrre3  10026  xrrege0  10029  xaddge0  10082  xle2add  10083  xlt2add  10084  fzass4  10266  fzrev  10288  elfz1b  10294  eluzgtdifelfzo  10411  fzocatel  10413  zsupcllemstep  10457  zsupcllemex  10458  zssinfcl  10460  suprzubdc  10464  exbtwnzlemex  10477  rebtwn2z  10482  modqid  10579  modqcyc  10589  modqaddabs  10592  modqaddmod  10593  mulqaddmodid  10594  modqadd2mod  10604  modqltm1p1mod  10606  modqsubmod  10612  modqsubmodmod  10613  modaddmodup  10617  modqmulmod  10619  modqmulmodr  10620  modqaddmulmod  10621  modqsubdir  10623  frec2uzisod  10637  uzennn  10666  iseqovex  10688  seqvalcd  10691  seq1g  10693  seqf  10694  seqovcd  10697  seqclg  10702  seqm1g  10704  seq3shft2  10711  seqshft2g  10712  monoord  10715  iseqf1olemnab  10731  seqf1oglem1  10749  seqf1og  10751  seqhomog  10760  seqfeq4g  10761  seq3distr  10762  expnegzap  10803  ltexp2a  10821  le2sq2  10845  bernneq  10890  expnlbnd2  10895  nn0ltexp2  10939  nn0opth2  10954  faclbnd  10971  bcval5  10993  hashcl  11011  hashen  11014  fihashdom  11033  hashunlem  11034  hashun  11035  hashxp  11056  fimaxq  11057  zfz1isolem1  11070  zfz1iso  11071  seq3coll  11072  sswrd  11088  ccatw2s1p2  11184  wrdind  11262  pfxccatin12lem1  11268  pfxccatin12lem3  11272  reuccatpfxs1lem  11286  cvg1nlemres  11504  cvg1n  11505  resqrexlemp1rp  11525  resqrexlemoverl  11540  resqrexlemex  11544  sqrtsq  11563  abslt  11607  absle  11608  abs3lem  11630  maxleastlt  11734  maxltsup  11737  fimaxre2  11746  negfi  11747  xrmaxleastlt  11775  xrmaxltsup  11777  xrmaxaddlem  11779  2clim  11820  climcn2  11828  addcn2  11829  mulcn2  11831  reccn2ap  11832  climge0  11844  climcau  11866  summodclem2  11901  summodc  11902  zsumdc  11903  fsumf1o  11909  fisumss  11911  fsum3cvg3  11915  fsumcl2lem  11917  fsumadd  11925  mptfzshft  11961  fsumrev  11962  fsummulc2  11967  fsumconst  11973  modfsummod  11977  fsumrelem  11990  binom  12003  cvgratnn  12050  mertenslemub  12053  prodmodclem2  12096  prodmodc  12097  zproddc  12098  fprodf1o  12107  fprodssdc  12109  fprodmul  12110  fprodcl2lem  12124  fprodrev  12138  fprodconst  12139  fprodap0  12140  fprodrec  12148  fprodap0f  12155  fprodle  12159  fprodmodd  12160  efcllem  12178  tanaddaplem  12257  moddvds  12318  dvdsflip  12370  oexpneg  12396  nn0o  12426  fldivndvdslt  12456  bitsfi  12476  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemeu  12536  dfgcd3  12539  dfgcd2  12543  dvdsmulgcd  12554  bezoutr  12561  nninfctlemfo  12569  lcmgcdlem  12607  coprmdvds2  12623  qredeu  12627  rpdvds  12629  cncongr1  12633  prmind2  12650  isprm5lem  12671  isprm6  12677  oddpwdclemdc  12703  nonsq  12737  hashdvds  12751  crth  12754  eulerthlemh  12761  prmdiveq  12766  hashgcdlem  12768  hashgcdeq  12770  nnnn0modprm0  12786  pclemub  12818  pceu  12826  pcmul  12832  pcqmul  12834  pcgcd1  12859  pc2dvds  12861  difsqpwdvds  12869  pcmpt  12874  prmpwdvds  12886  1arith  12898  mul4sq  12925  4sqlemafi  12926  4sqlemffi  12927  4sqexercise2  12930  ennnfonelemg  12982  ennnfonelemex  12993  ennnfonelemrnh  12995  ennnfonelemf1  12997  ennnfonelemrn  12998  ennnfonelemdm  12999  ennnfonelemim  13003  ennnfone  13004  ctinf  13009  ctiunctlemfo  13018  nninfdclemcl  13027  nninfdclemf  13028  nninfdclemp1  13029  unbendc  13033  isstruct2r  13051  setscom  13080  ercpbl  13372  opifismgmdc  13412  grpinvalem  13426  igsumvalx  13430  gsumfzval  13432  gsumval2  13438  sgrppropd  13454  prdssgrpd  13456  mndpropd  13481  issubmnd  13483  submnd0  13485  prdsmndd  13489  mhmf1o  13511  subsubm  13524  0mhm  13527  resmhm  13528  mhmco  13531  mhmima  13532  mhmeql  13533  gsumfzz  13536  gsumwsubmcl  13537  gsumfzcl  13540  grprcan  13578  grpinvid1  13593  grpinvid2  13594  grplcan  13603  grplmulf1o  13615  grpnpncan0  13637  dfgrp3mlem  13639  grplactcnv  13643  pwssub  13654  mulgval  13667  mulgfng  13669  mulgnngsum  13672  mulg1  13674  mulgnnp1  13675  mulgneg  13685  mulgnndir  13696  mulgdirlem  13698  mulgnn0ass  13703  mulgass  13704  subgmulg  13733  issubg4m  13738  subsubg  13742  subgintm  13743  isnsg3  13752  eqgcpbl  13773  ghmeql  13812  ghmnsgima  13813  ghmnsgpreima  13814  ghmf1  13818  ghmf1o  13820  conjghm  13821  qusghm  13827  ablpncan3  13862  invghm  13874  eqgabl  13875  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  rngpropd  13926  imasrng  13927  qusrng  13929  srglmhm  13964  srgrmhm  13965  ringpropd  14009  ringlghm  14032  ringrghm  14033  imasring  14035  qusring2  14037  opprrngbg  14049  dvdsrvald  14065  dvdsrd  14066  dvdsrex  14070  dvdsrtr  14073  unitpropdg  14120  rhmopp  14148  isnzr2  14156  issubrng2  14182  subrngintm  14184  subsubrng  14186  subrgintm  14215  subsubrg  14217  rhmpropd  14226  aprap  14258  lmodprop2d  14320  rmodislmod  14323  lssvacl  14337  lssvsubcl  14338  lssvscl  14347  islss3  14351  lss1d  14355  rnglidlmcl  14452  2idlcpblrng  14495  crngridl  14502  expghmap  14579  mulgghm2  14580  mulgrhm  14581  znf1o  14623  znleval  14625  znidom  14629  znidomb  14630  znunit  14631  mplsubgfilemcl  14671  iuncld  14797  ssnei2  14839  topssnei  14844  restopnb  14863  cnfval  14876  cnpfval  14877  iscnp4  14900  cnptopco  14904  cncnpi  14910  cncnp  14912  cnconst2  14915  cnrest2  14918  cnptoprest  14921  cnptoprest2  14922  cnpdis  14924  lmss  14928  lmtopcnp  14932  neitx  14950  txcnp  14953  txrest  14958  txdis1cn  14960  txlm  14961  cnmpt21  14973  imasnopn  14981  xmetres2  15061  blvalps  15070  blval  15071  elbl2ps  15074  elbl2  15075  blhalf  15090  blssexps  15111  blssex  15112  ssblex  15113  blin2  15114  bdmetval  15182  xmetxp  15189  xmettx  15192  metcnpi3  15199  txmetcnp  15200  addcncntoplem  15243  fsumcncntop  15249  elcncf2  15256  mulc1cncf  15271  cncfco  15273  cncfmet  15274  cncfmptc  15278  mulcncf  15290  dedekindeulemub  15300  dedekindeulemloc  15301  dedekindeulemlu  15303  dedekindeu  15305  dedekindicclemub  15309  dedekindicclemloc  15310  dedekindicclemlu  15312  dedekindicclemicc  15314  dedekindicc  15315  ivthinclemlopn  15318  ivthinclemuopn  15320  dich0  15334  limcimo  15347  cnplimccntop  15352  limccnp2lem  15358  limccnp2cntop  15359  dvfvalap  15363  dveflem  15408  plycolemc  15440  plyco  15441  plyrecj  15445  reeff1olem  15453  reeff1oleme  15454  eflt  15457  sin0pilem2  15464  pilem3  15465  ioocosf1o  15536  cxplt  15598  cxple  15599  cxplt3  15602  apcxp2  15621  rprelogbmul  15637  rprelogbdiv  15639  logbgt0b  15648  logbgcd1irrap  15652  mpodvdsmulf1o  15672  fsumdvdsmul  15673  lgsdir2lem5  15719  lgsdi  15724  lgsne0  15725  gausslemma2dlem1f1o  15747  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem2  15769  lgsquad2  15770  2sqlem6  15807  2sqlem8  15810  2sqlem9  15811  2sqlem10  15812  upgredg  15950  usgredg4  16021  uspgredg2vlem  16026  iswlkg  16050  upgriswlkdc  16081  upgr2wlkdc  16096  nnti  16385  pwtrufal  16392  pwf1oexmid  16394  sssneq  16397  qdencn  16425  cvgcmp2n  16431  trilpolemlt1  16439  trirec0  16442  redc0  16455  reap0  16456  cndcap  16457  nconstwlpolemgt0  16462  neap0mkv  16467  supfz  16469  inffz  16470