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:  simp1rr  1065  simp2rr  1069  simp3rr  1073  disjiun  4029  reg2exmidlema  4571  reg3exmidlemwe  4616  nnsucpred  4654  iotam  5251  fvmptt  5656  fcof1  5833  fliftfun  5846  isotr  5866  riotass2  5907  acexmidlemab  5919  ovmpodf  6058  fnmpoovd  6282  1stconst  6288  2ndconst  6289  cnvf1olem  6291  f1od2  6302  smoiso  6369  tfrcldm  6430  tfrcl  6431  nntr2  6570  swoer  6629  erinxp  6677  ecopovsymg  6702  th3qlem1  6705  f1imaen2g  6861  pw2f1odclem  6904  mapdom1g  6917  fict  6938  fidifsnen  6940  dif1enen  6950  fiunsnnn  6951  fisbth  6953  findcard2d  6961  findcard2sd  6962  diffifi  6964  ac6sfi  6968  fimax2gtri  6971  nnwetri  6986  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fisseneq  7004  ssfirab  7006  fidcenumlemrk  7029  fidcenumlemr  7030  sbthlemi6  7037  sbthlemi8  7039  isbth  7042  fiuni  7053  supmaxti  7079  infminti  7102  ordiso2  7110  eldju2ndl  7147  eldju2ndr  7148  omp1eomlem  7169  difinfsnlem  7174  difinfinf  7176  ctmlemr  7183  ctssdccl  7186  nninfninc  7198  fodjum  7221  fodju0  7222  omniwomnimkv  7242  exmidfodomrlemrALT  7282  acfun  7290  exmidaclem  7291  netap  7337  exmidmotap  7344  ccfunen  7347  cc1  7348  cc2lem  7349  dfplpq2  7438  dfmpq2  7439  mulpipqqs  7457  distrnqg  7471  enq0sym  7516  enq0tr  7518  distrnq0  7543  prarloclem3  7581  genplt2i  7594  addlocpr  7620  prmuloc  7650  distrlem1prl  7666  distrlem1pru  7667  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  ltaprg  7703  prplnqu  7704  addextpr  7705  recexprlemdisj  7714  recexprlemloc  7715  aptiprleml  7723  aptiprlemu  7724  ltmprr  7726  archpr  7727  cauappcvgprlemopl  7730  cauappcvgprlemopu  7732  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlem1  7743  cauappcvgprlemlim  7745  caucvgprlemnkj  7750  caucvgprlemopl  7753  caucvgprlemopu  7755  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemnjltk  7775  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemopu  7783  caucvgprprlemdisj  7786  caucvgprprlemloc  7787  caucvgprprlemaddq  7792  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemex  7806  suplocexprlemub  7807  recexgt0sr  7857  mulgt0sr  7862  prsrriota  7872  suplocsrlem  7892  addcnsr  7918  mulcnsr  7919  mulcnsrec  7927  axmulcom  7955  rereceu  7973  axarch  7975  axcaucvglemres  7983  axpre-suploclemres  7985  lelttr  8132  ltletr  8133  addcan  8223  addcan2  8224  addsub4  8286  ltadd2  8463  le2add  8488  lt2add  8489  lt2sub  8504  le2sub  8505  eqord1  8527  rereim  8630  apreap  8631  apreim  8647  mulreim  8648  apcotr  8651  apadd1  8652  addext  8654  apneg  8655  mulext1  8656  mulext  8658  ltleap  8676  aprcl  8690  mulap0  8698  mulcanapd  8705  recapb  8715  rec11ap  8754  rec11rap  8755  divdivdivap  8757  ddcanap  8770  divadddivap  8771  prodgt0gt0  8895  prodgt0  8896  prodge0  8898  lemulge11  8910  lt2mul2div  8923  ltrec  8927  lerec  8928  lerec2  8933  ledivp1  8947  mulle0r  8988  nn0ge0div  9430  suprzclex  9441  qapne  9730  xrlelttr  9898  xrltletr  9899  xrre3  9914  xrrege0  9917  xaddge0  9970  xle2add  9971  xlt2add  9972  fzass4  10154  fzrev  10176  elfz1b  10182  eluzgtdifelfzo  10290  fzocatel  10292  zsupcllemstep  10336  zsupcllemex  10337  zssinfcl  10339  suprzubdc  10343  exbtwnzlemex  10356  rebtwn2z  10361  modqid  10458  modqcyc  10468  modqaddabs  10471  modqaddmod  10472  mulqaddmodid  10473  modqadd2mod  10483  modqltm1p1mod  10485  modqsubmod  10491  modqsubmodmod  10492  modaddmodup  10496  modqmulmod  10498  modqmulmodr  10499  modqaddmulmod  10500  modqsubdir  10502  frec2uzisod  10516  uzennn  10545  iseqovex  10567  seqvalcd  10570  seq1g  10572  seqf  10573  seqovcd  10576  seqclg  10581  seqm1g  10583  seq3shft2  10590  seqshft2g  10591  monoord  10594  iseqf1olemnab  10610  seqf1oglem1  10628  seqf1og  10630  seqhomog  10639  seqfeq4g  10640  seq3distr  10641  expnegzap  10682  ltexp2a  10700  le2sq2  10724  bernneq  10769  expnlbnd2  10774  nn0ltexp2  10818  nn0opth2  10833  faclbnd  10850  bcval5  10872  hashcl  10890  hashen  10893  fihashdom  10912  hashunlem  10913  hashun  10914  hashxp  10935  fimaxq  10936  zfz1isolem1  10949  zfz1iso  10950  seq3coll  10951  sswrd  10961  cvg1nlemres  11167  cvg1n  11168  resqrexlemp1rp  11188  resqrexlemoverl  11203  resqrexlemex  11207  sqrtsq  11226  abslt  11270  absle  11271  abs3lem  11293  maxleastlt  11397  maxltsup  11400  fimaxre2  11409  negfi  11410  xrmaxleastlt  11438  xrmaxltsup  11440  xrmaxaddlem  11442  2clim  11483  climcn2  11491  addcn2  11492  mulcn2  11494  reccn2ap  11495  climge0  11507  climcau  11529  summodclem2  11564  summodc  11565  zsumdc  11566  fsumf1o  11572  fisumss  11574  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  mptfzshft  11624  fsumrev  11625  fsummulc2  11630  fsumconst  11636  modfsummod  11640  fsumrelem  11653  binom  11666  cvgratnn  11713  mertenslemub  11716  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodf1o  11770  fprodssdc  11772  fprodmul  11773  fprodcl2lem  11787  fprodrev  11801  fprodconst  11802  fprodap0  11803  fprodrec  11811  fprodap0f  11818  fprodle  11822  fprodmodd  11823  efcllem  11841  tanaddaplem  11920  moddvds  11981  dvdsflip  12033  oexpneg  12059  nn0o  12089  fldivndvdslt  12119  bitsfi  12139  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemeu  12199  dfgcd3  12202  dfgcd2  12206  dvdsmulgcd  12217  bezoutr  12224  nninfctlemfo  12232  lcmgcdlem  12270  coprmdvds2  12286  qredeu  12290  rpdvds  12292  cncongr1  12296  prmind2  12313  isprm5lem  12334  isprm6  12340  oddpwdclemdc  12366  nonsq  12400  hashdvds  12414  crth  12417  eulerthlemh  12424  prmdiveq  12429  hashgcdlem  12431  hashgcdeq  12433  nnnn0modprm0  12449  pclemub  12481  pceu  12489  pcmul  12495  pcqmul  12497  pcgcd1  12522  pc2dvds  12524  difsqpwdvds  12532  pcmpt  12537  prmpwdvds  12549  1arith  12561  mul4sq  12588  4sqlemafi  12589  4sqlemffi  12590  4sqexercise2  12593  ennnfonelemg  12645  ennnfonelemex  12656  ennnfonelemrnh  12658  ennnfonelemf1  12660  ennnfonelemrn  12661  ennnfonelemdm  12662  ennnfonelemim  12666  ennnfone  12667  ctinf  12672  ctiunctlemfo  12681  nninfdclemcl  12690  nninfdclemf  12691  nninfdclemp1  12692  unbendc  12696  isstruct2r  12714  setscom  12743  ercpbl  13033  opifismgmdc  13073  grpinvalem  13087  igsumvalx  13091  gsumfzval  13093  gsumval2  13099  sgrppropd  13115  prdssgrpd  13117  mndpropd  13142  issubmnd  13144  submnd0  13146  prdsmndd  13150  mhmf1o  13172  subsubm  13185  0mhm  13188  resmhm  13189  mhmco  13192  mhmima  13193  mhmeql  13194  gsumfzz  13197  gsumwsubmcl  13198  gsumfzcl  13201  grprcan  13239  grpinvid1  13254  grpinvid2  13255  grplcan  13264  grplmulf1o  13276  grpnpncan0  13298  dfgrp3mlem  13300  grplactcnv  13304  pwssub  13315  mulgval  13328  mulgfng  13330  mulgnngsum  13333  mulg1  13335  mulgnnp1  13336  mulgneg  13346  mulgnndir  13357  mulgdirlem  13359  mulgnn0ass  13364  mulgass  13365  subgmulg  13394  issubg4m  13399  subsubg  13403  subgintm  13404  isnsg3  13413  eqgcpbl  13434  ghmeql  13473  ghmnsgima  13474  ghmnsgpreima  13475  ghmf1  13479  ghmf1o  13481  conjghm  13482  qusghm  13488  ablpncan3  13523  invghm  13535  eqgabl  13536  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  rngpropd  13587  imasrng  13588  qusrng  13590  srglmhm  13625  srgrmhm  13626  ringpropd  13670  ringlghm  13693  ringrghm  13694  imasring  13696  qusring2  13698  opprrngbg  13710  dvdsrvald  13725  dvdsrd  13726  dvdsrex  13730  dvdsrtr  13733  unitpropdg  13780  rhmopp  13808  isnzr2  13816  issubrng2  13842  subrngintm  13844  subsubrng  13846  subrgintm  13875  subsubrg  13877  rhmpropd  13886  aprap  13918  lmodprop2d  13980  rmodislmod  13983  lssvacl  13997  lssvsubcl  13998  lssvscl  14007  islss3  14011  lss1d  14015  rnglidlmcl  14112  2idlcpblrng  14155  crngridl  14162  expghmap  14239  mulgghm2  14240  mulgrhm  14241  znf1o  14283  znleval  14285  znidom  14289  znidomb  14290  znunit  14291  iuncld  14435  ssnei2  14477  topssnei  14482  restopnb  14501  cnfval  14514  cnpfval  14515  iscnp4  14538  cnptopco  14542  cncnpi  14548  cncnp  14550  cnconst2  14553  cnrest2  14556  cnptoprest  14559  cnptoprest2  14560  cnpdis  14562  lmss  14566  lmtopcnp  14570  neitx  14588  txcnp  14591  txrest  14596  txdis1cn  14598  txlm  14599  cnmpt21  14611  imasnopn  14619  xmetres2  14699  blvalps  14708  blval  14709  elbl2ps  14712  elbl2  14713  blhalf  14728  blssexps  14749  blssex  14750  ssblex  14751  blin2  14752  bdmetval  14820  xmetxp  14827  xmettx  14830  metcnpi3  14837  txmetcnp  14838  addcncntoplem  14881  fsumcncntop  14887  elcncf2  14894  mulc1cncf  14909  cncfco  14911  cncfmet  14912  cncfmptc  14916  mulcncf  14928  dedekindeulemub  14938  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeu  14943  dedekindicclemub  14947  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicclemicc  14952  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemuopn  14958  dich0  14972  limcimo  14985  cnplimccntop  14990  limccnp2lem  14996  limccnp2cntop  14997  dvfvalap  15001  dveflem  15046  plycolemc  15078  plyco  15079  plyrecj  15083  reeff1olem  15091  reeff1oleme  15092  eflt  15095  sin0pilem2  15102  pilem3  15103  ioocosf1o  15174  cxplt  15236  cxple  15237  cxplt3  15240  apcxp2  15259  rprelogbmul  15275  rprelogbdiv  15277  logbgt0b  15286  logbgcd1irrap  15290  mpodvdsmulf1o  15310  fsumdvdsmul  15311  lgsdir2lem5  15357  lgsdi  15362  lgsne0  15363  gausslemma2dlem1f1o  15385  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem2  15407  lgsquad2  15408  2sqlem6  15445  2sqlem8  15448  2sqlem9  15449  2sqlem10  15450  nnti  15723  pwtrufal  15728  pwf1oexmid  15730  sssneq  15733  qdencn  15758  cvgcmp2n  15764  trilpolemlt1  15772  trirec0  15775  redc0  15788  reap0  15789  cndcap  15790  nconstwlpolemgt0  15795  neap0mkv  15800  supfz  15802  inffz  15803