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  1066  simp2rr  1070  simp3rr  1074  invdisjrab  4041  disjiun  4042  reg2exmidlema  4586  reg3exmidlemwe  4631  nnsucpred  4669  iotam  5268  fvmptt  5678  fcof1  5859  fliftfun  5872  isotr  5892  riotass2  5933  acexmidlemab  5945  ovmpodf  6084  fnmpoovd  6308  1stconst  6314  2ndconst  6315  cnvf1olem  6317  f1od2  6328  smoiso  6395  tfrcldm  6456  tfrcl  6457  nntr2  6596  swoer  6655  erinxp  6703  ecopovsymg  6728  th3qlem1  6731  f1imaen2g  6892  pw2f1odclem  6938  mapdom1g  6951  fict  6972  fidifsnen  6974  dif1enen  6984  fiunsnnn  6985  fisbth  6987  findcard2d  6995  findcard2sd  6996  diffifi  6998  ac6sfi  7002  fimax2gtri  7005  nnwetri  7020  unsnfi  7023  unsnfidcex  7024  unsnfidcel  7025  fisseneq  7038  ssfirab  7040  fidcenumlemrk  7063  fidcenumlemr  7064  sbthlemi6  7071  sbthlemi8  7073  isbth  7076  fiuni  7087  supmaxti  7113  infminti  7136  ordiso2  7144  eldju2ndl  7181  eldju2ndr  7182  omp1eomlem  7203  difinfsnlem  7208  difinfinf  7210  ctmlemr  7217  ctssdccl  7220  nninfninc  7232  fodjum  7255  fodju0  7256  omniwomnimkv  7276  exmidfodomrlemrALT  7318  acfun  7326  exmidaclem  7327  netap  7373  exmidmotap  7380  ccfunen  7383  cc1  7384  cc2lem  7385  dfplpq2  7474  dfmpq2  7475  mulpipqqs  7493  distrnqg  7507  enq0sym  7552  enq0tr  7554  distrnq0  7579  prarloclem3  7617  genplt2i  7630  addlocpr  7656  prmuloc  7686  distrlem1prl  7702  distrlem1pru  7703  ltexprlemopl  7721  ltexprlemopu  7723  ltexprlemfl  7729  ltexprlemrl  7730  ltexprlemfu  7731  ltexprlemru  7732  addcanprleml  7734  addcanprlemu  7735  ltaprg  7739  prplnqu  7740  addextpr  7741  recexprlemdisj  7750  recexprlemloc  7751  aptiprleml  7759  aptiprlemu  7760  ltmprr  7762  archpr  7763  cauappcvgprlemopl  7766  cauappcvgprlemopu  7768  cauappcvgprlemdisj  7771  cauappcvgprlemloc  7772  cauappcvgprlem1  7779  cauappcvgprlemlim  7781  caucvgprlemnkj  7786  caucvgprlemopl  7789  caucvgprlemopu  7791  caucvgprlemdisj  7794  caucvgprlemloc  7795  caucvgprprlemnkltj  7809  caucvgprprlemnkeqj  7810  caucvgprprlemnjltk  7811  caucvgprprlemml  7814  caucvgprprlemmu  7815  caucvgprprlemopl  7817  caucvgprprlemopu  7819  caucvgprprlemdisj  7822  caucvgprprlemloc  7823  caucvgprprlemaddq  7828  suplocexprlemrl  7837  suplocexprlemmu  7838  suplocexprlemru  7839  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemex  7842  suplocexprlemub  7843  recexgt0sr  7893  mulgt0sr  7898  prsrriota  7908  suplocsrlem  7928  addcnsr  7954  mulcnsr  7955  mulcnsrec  7963  axmulcom  7991  rereceu  8009  axarch  8011  axcaucvglemres  8019  axpre-suploclemres  8021  lelttr  8168  ltletr  8169  addcan  8259  addcan2  8260  addsub4  8322  ltadd2  8499  le2add  8524  lt2add  8525  lt2sub  8540  le2sub  8541  eqord1  8563  rereim  8666  apreap  8667  apreim  8683  mulreim  8684  apcotr  8687  apadd1  8688  addext  8690  apneg  8691  mulext1  8692  mulext  8694  ltleap  8712  aprcl  8726  mulap0  8734  mulcanapd  8741  recapb  8751  rec11ap  8790  rec11rap  8791  divdivdivap  8793  ddcanap  8806  divadddivap  8807  prodgt0gt0  8931  prodgt0  8932  prodge0  8934  lemulge11  8946  lt2mul2div  8959  ltrec  8963  lerec  8964  lerec2  8969  ledivp1  8983  mulle0r  9024  nn0ge0div  9467  suprzclex  9478  qapne  9767  xrlelttr  9935  xrltletr  9936  xrre3  9951  xrrege0  9954  xaddge0  10007  xle2add  10008  xlt2add  10009  fzass4  10191  fzrev  10213  elfz1b  10219  eluzgtdifelfzo  10333  fzocatel  10335  zsupcllemstep  10379  zsupcllemex  10380  zssinfcl  10382  suprzubdc  10386  exbtwnzlemex  10399  rebtwn2z  10404  modqid  10501  modqcyc  10511  modqaddabs  10514  modqaddmod  10515  mulqaddmodid  10516  modqadd2mod  10526  modqltm1p1mod  10528  modqsubmod  10534  modqsubmodmod  10535  modaddmodup  10539  modqmulmod  10541  modqmulmodr  10542  modqaddmulmod  10543  modqsubdir  10545  frec2uzisod  10559  uzennn  10588  iseqovex  10610  seqvalcd  10613  seq1g  10615  seqf  10616  seqovcd  10619  seqclg  10624  seqm1g  10626  seq3shft2  10633  seqshft2g  10634  monoord  10637  iseqf1olemnab  10653  seqf1oglem1  10671  seqf1og  10673  seqhomog  10682  seqfeq4g  10683  seq3distr  10684  expnegzap  10725  ltexp2a  10743  le2sq2  10767  bernneq  10812  expnlbnd2  10817  nn0ltexp2  10861  nn0opth2  10876  faclbnd  10893  bcval5  10915  hashcl  10933  hashen  10936  fihashdom  10955  hashunlem  10956  hashun  10957  hashxp  10978  fimaxq  10979  zfz1isolem1  10992  zfz1iso  10993  seq3coll  10994  sswrd  11010  ccatw2s1p2  11105  cvg1nlemres  11340  cvg1n  11341  resqrexlemp1rp  11361  resqrexlemoverl  11376  resqrexlemex  11380  sqrtsq  11399  abslt  11443  absle  11444  abs3lem  11466  maxleastlt  11570  maxltsup  11573  fimaxre2  11582  negfi  11583  xrmaxleastlt  11611  xrmaxltsup  11613  xrmaxaddlem  11615  2clim  11656  climcn2  11664  addcn2  11665  mulcn2  11667  reccn2ap  11668  climge0  11680  climcau  11702  summodclem2  11737  summodc  11738  zsumdc  11739  fsumf1o  11745  fisumss  11747  fsum3cvg3  11751  fsumcl2lem  11753  fsumadd  11761  mptfzshft  11797  fsumrev  11798  fsummulc2  11803  fsumconst  11809  modfsummod  11813  fsumrelem  11826  binom  11839  cvgratnn  11886  mertenslemub  11889  prodmodclem2  11932  prodmodc  11933  zproddc  11934  fprodf1o  11943  fprodssdc  11945  fprodmul  11946  fprodcl2lem  11960  fprodrev  11974  fprodconst  11975  fprodap0  11976  fprodrec  11984  fprodap0f  11991  fprodle  11995  fprodmodd  11996  efcllem  12014  tanaddaplem  12093  moddvds  12154  dvdsflip  12206  oexpneg  12232  nn0o  12262  fldivndvdslt  12292  bitsfi  12312  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemeu  12372  dfgcd3  12375  dfgcd2  12379  dvdsmulgcd  12390  bezoutr  12397  nninfctlemfo  12405  lcmgcdlem  12443  coprmdvds2  12459  qredeu  12463  rpdvds  12465  cncongr1  12469  prmind2  12486  isprm5lem  12507  isprm6  12513  oddpwdclemdc  12539  nonsq  12573  hashdvds  12587  crth  12590  eulerthlemh  12597  prmdiveq  12602  hashgcdlem  12604  hashgcdeq  12606  nnnn0modprm0  12622  pclemub  12654  pceu  12662  pcmul  12668  pcqmul  12670  pcgcd1  12695  pc2dvds  12697  difsqpwdvds  12705  pcmpt  12710  prmpwdvds  12722  1arith  12734  mul4sq  12761  4sqlemafi  12762  4sqlemffi  12763  4sqexercise2  12766  ennnfonelemg  12818  ennnfonelemex  12829  ennnfonelemrnh  12831  ennnfonelemf1  12833  ennnfonelemrn  12834  ennnfonelemdm  12835  ennnfonelemim  12839  ennnfone  12840  ctinf  12845  ctiunctlemfo  12854  nninfdclemcl  12863  nninfdclemf  12864  nninfdclemp1  12865  unbendc  12869  isstruct2r  12887  setscom  12916  ercpbl  13207  opifismgmdc  13247  grpinvalem  13261  igsumvalx  13265  gsumfzval  13267  gsumval2  13273  sgrppropd  13289  prdssgrpd  13291  mndpropd  13316  issubmnd  13318  submnd0  13320  prdsmndd  13324  mhmf1o  13346  subsubm  13359  0mhm  13362  resmhm  13363  mhmco  13366  mhmima  13367  mhmeql  13368  gsumfzz  13371  gsumwsubmcl  13372  gsumfzcl  13375  grprcan  13413  grpinvid1  13428  grpinvid2  13429  grplcan  13438  grplmulf1o  13450  grpnpncan0  13472  dfgrp3mlem  13474  grplactcnv  13478  pwssub  13489  mulgval  13502  mulgfng  13504  mulgnngsum  13507  mulg1  13509  mulgnnp1  13510  mulgneg  13520  mulgnndir  13531  mulgdirlem  13533  mulgnn0ass  13538  mulgass  13539  subgmulg  13568  issubg4m  13573  subsubg  13577  subgintm  13578  isnsg3  13587  eqgcpbl  13608  ghmeql  13647  ghmnsgima  13648  ghmnsgpreima  13649  ghmf1  13653  ghmf1o  13655  conjghm  13656  qusghm  13662  ablpncan3  13697  invghm  13709  eqgabl  13710  gsumfzreidx  13717  gsumfzsubmcl  13718  gsumfzmptfidmadd  13719  gsumfzmhm  13723  rngpropd  13761  imasrng  13762  qusrng  13764  srglmhm  13799  srgrmhm  13800  ringpropd  13844  ringlghm  13867  ringrghm  13868  imasring  13870  qusring2  13872  opprrngbg  13884  dvdsrvald  13899  dvdsrd  13900  dvdsrex  13904  dvdsrtr  13907  unitpropdg  13954  rhmopp  13982  isnzr2  13990  issubrng2  14016  subrngintm  14018  subsubrng  14020  subrgintm  14049  subsubrg  14051  rhmpropd  14060  aprap  14092  lmodprop2d  14154  rmodislmod  14157  lssvacl  14171  lssvsubcl  14172  lssvscl  14181  islss3  14185  lss1d  14189  rnglidlmcl  14286  2idlcpblrng  14329  crngridl  14336  expghmap  14413  mulgghm2  14414  mulgrhm  14415  znf1o  14457  znleval  14459  znidom  14463  znidomb  14464  znunit  14465  mplsubgfilemcl  14505  iuncld  14631  ssnei2  14673  topssnei  14678  restopnb  14697  cnfval  14710  cnpfval  14711  iscnp4  14734  cnptopco  14738  cncnpi  14744  cncnp  14746  cnconst2  14749  cnrest2  14752  cnptoprest  14755  cnptoprest2  14756  cnpdis  14758  lmss  14762  lmtopcnp  14766  neitx  14784  txcnp  14787  txrest  14792  txdis1cn  14794  txlm  14795  cnmpt21  14807  imasnopn  14815  xmetres2  14895  blvalps  14904  blval  14905  elbl2ps  14908  elbl2  14909  blhalf  14924  blssexps  14945  blssex  14946  ssblex  14947  blin2  14948  bdmetval  15016  xmetxp  15023  xmettx  15026  metcnpi3  15033  txmetcnp  15034  addcncntoplem  15077  fsumcncntop  15083  elcncf2  15090  mulc1cncf  15105  cncfco  15107  cncfmet  15108  cncfmptc  15112  mulcncf  15124  dedekindeulemub  15134  dedekindeulemloc  15135  dedekindeulemlu  15137  dedekindeu  15139  dedekindicclemub  15143  dedekindicclemloc  15144  dedekindicclemlu  15146  dedekindicclemicc  15148  dedekindicc  15149  ivthinclemlopn  15152  ivthinclemuopn  15154  dich0  15168  limcimo  15181  cnplimccntop  15186  limccnp2lem  15192  limccnp2cntop  15193  dvfvalap  15197  dveflem  15242  plycolemc  15274  plyco  15275  plyrecj  15279  reeff1olem  15287  reeff1oleme  15288  eflt  15291  sin0pilem2  15298  pilem3  15299  ioocosf1o  15370  cxplt  15432  cxple  15433  cxplt3  15436  apcxp2  15455  rprelogbmul  15471  rprelogbdiv  15473  logbgt0b  15482  logbgcd1irrap  15486  mpodvdsmulf1o  15506  fsumdvdsmul  15507  lgsdir2lem5  15553  lgsdi  15558  lgsne0  15559  gausslemma2dlem1f1o  15581  lgseisenlem2  15592  lgsquadlem1  15598  lgsquadlem2  15599  lgsquadlem3  15600  lgsquad2lem2  15603  lgsquad2  15604  2sqlem6  15641  2sqlem8  15644  2sqlem9  15645  2sqlem10  15646  nnti  16003  pwtrufal  16008  pwf1oexmid  16010  sssneq  16013  qdencn  16040  cvgcmp2n  16046  trilpolemlt1  16054  trirec0  16057  redc0  16070  reap0  16071  cndcap  16072  nconstwlpolemgt0  16077  neap0mkv  16082  supfz  16084  inffz  16085