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  989  simp1rr  1089  simp2rr  1093  simp3rr  1097  elpr2elpr  3859  invdisjrab  4082  disjiun  4083  reg2exmidlema  4632  reg3exmidlemwe  4677  nnsucpred  4715  iotam  5318  fvmptt  5738  fcof1  5924  fliftfun  5937  isotr  5957  riotass2  6000  acexmidlemab  6012  ovmpodf  6153  fnmpoovd  6380  1stconst  6386  2ndconst  6387  cnvf1olem  6389  f1od2  6400  smoiso  6468  tfrcldm  6529  tfrcl  6530  nntr2  6671  swoer  6730  erinxp  6778  ecopovsymg  6803  th3qlem1  6806  f1imaen2g  6967  pw2f1odclem  7020  mapdom1g  7033  fict  7055  fidifsnen  7057  dif1enen  7069  fiunsnnn  7070  fisbth  7072  findcard2d  7080  findcard2sd  7081  diffifi  7083  ac6sfi  7087  fimax2gtri  7091  nnwetri  7108  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fisseneq  7127  ssfirab  7129  exmidssfi  7131  fidcenumlemrk  7153  fidcenumlemr  7154  sbthlemi6  7161  sbthlemi8  7163  isbth  7166  fiuni  7177  supmaxti  7203  infminti  7226  ordiso2  7234  eldju2ndl  7271  eldju2ndr  7272  omp1eomlem  7293  difinfsnlem  7298  difinfinf  7300  ctmlemr  7307  ctssdccl  7310  nninfninc  7322  fodjum  7345  fodju0  7346  omniwomnimkv  7366  exmidfodomrlemrALT  7414  acfun  7422  exmidaclem  7423  netap  7473  exmidmotap  7480  ccfunen  7483  cc1  7484  cc2lem  7485  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  distrnqg  7607  enq0sym  7652  enq0tr  7654  distrnq0  7679  prarloclem3  7717  genplt2i  7730  addlocpr  7756  prmuloc  7786  distrlem1prl  7802  distrlem1pru  7803  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprg  7839  prplnqu  7840  addextpr  7841  recexprlemdisj  7850  recexprlemloc  7851  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  archpr  7863  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemdisj  7922  caucvgprprlemloc  7923  caucvgprprlemaddq  7928  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  recexgt0sr  7993  mulgt0sr  7998  prsrriota  8008  suplocsrlem  8028  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axmulcom  8091  rereceu  8109  axarch  8111  axcaucvglemres  8119  axpre-suploclemres  8121  lelttr  8268  ltletr  8269  addcan  8359  addcan2  8360  addsub4  8422  ltadd2  8599  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  eqord1  8663  rereim  8766  apreap  8767  apreim  8783  mulreim  8784  apcotr  8787  apadd1  8788  addext  8790  apneg  8791  mulext1  8792  mulext  8794  ltleap  8812  aprcl  8826  mulap0  8834  mulcanapd  8841  recapb  8851  rec11ap  8890  rec11rap  8891  divdivdivap  8893  ddcanap  8906  divadddivap  8907  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  lerec2  9069  ledivp1  9083  mulle0r  9124  nn0ge0div  9567  suprzclex  9578  qapne  9873  xrlelttr  10041  xrltletr  10042  xrre3  10057  xrrege0  10060  xaddge0  10113  xle2add  10114  xlt2add  10115  fzass4  10297  fzrev  10319  elfz1b  10325  eluzgtdifelfzo  10443  fzocatel  10445  zsupcllemstep  10490  zsupcllemex  10491  zssinfcl  10493  suprzubdc  10497  exbtwnzlemex  10510  rebtwn2z  10515  modqid  10612  modqcyc  10622  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqadd2mod  10637  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modaddmodup  10650  modqmulmod  10652  modqmulmodr  10653  modqaddmulmod  10654  modqsubdir  10656  frec2uzisod  10670  uzennn  10699  iseqovex  10721  seqvalcd  10724  seq1g  10726  seqf  10727  seqovcd  10730  seqclg  10735  seqm1g  10737  seq3shft2  10744  seqshft2g  10745  monoord  10748  iseqf1olemnab  10764  seqf1oglem1  10782  seqf1og  10784  seqhomog  10793  seqfeq4g  10794  seq3distr  10795  expnegzap  10836  ltexp2a  10854  le2sq2  10878  bernneq  10923  expnlbnd2  10928  nn0ltexp2  10972  nn0opth2  10987  faclbnd  11004  bcval5  11026  hashcl  11044  hashen  11047  fihashdom  11067  hashunlem  11068  hashun  11069  hashxp  11091  fimaxq  11092  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  sswrd  11123  ccatw2s1p1g  11223  ccatw2s1p2  11224  ccat2s1fstg  11226  wrdind  11304  pfxccatin12lem1  11310  pfxccatin12lem3  11314  reuccatpfxs1lem  11328  cvg1nlemres  11547  cvg1n  11548  resqrexlemp1rp  11568  resqrexlemoverl  11583  resqrexlemex  11587  sqrtsq  11606  abslt  11650  absle  11651  abs3lem  11673  maxleastlt  11777  maxltsup  11780  fimaxre2  11789  negfi  11790  xrmaxleastlt  11818  xrmaxltsup  11820  xrmaxaddlem  11822  2clim  11863  climcn2  11871  addcn2  11872  mulcn2  11874  reccn2ap  11875  climge0  11887  climcau  11909  fzf1o  11938  summodclem2  11945  summodc  11946  zsumdc  11947  fsumf1o  11953  fisumss  11955  fsum3cvg3  11959  fsumcl2lem  11961  fsumadd  11969  mptfzshft  12005  fsumrev  12006  fsummulc2  12011  fsumconst  12017  modfsummod  12021  fsumrelem  12034  binom  12047  cvgratnn  12094  mertenslemub  12097  prodmodclem2  12140  prodmodc  12141  zproddc  12142  fprodf1o  12151  fprodssdc  12153  fprodmul  12154  fprodcl2lem  12168  fprodrev  12182  fprodconst  12183  fprodap0  12184  fprodrec  12192  fprodap0f  12199  fprodle  12203  fprodmodd  12204  efcllem  12222  tanaddaplem  12301  moddvds  12362  dvdsflip  12414  oexpneg  12440  nn0o  12470  fldivndvdslt  12500  bitsfi  12520  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlemeu  12580  dfgcd3  12583  dfgcd2  12587  dvdsmulgcd  12598  bezoutr  12605  nninfctlemfo  12613  lcmgcdlem  12651  coprmdvds2  12667  qredeu  12671  rpdvds  12673  cncongr1  12677  prmind2  12694  isprm5lem  12715  isprm6  12721  oddpwdclemdc  12747  nonsq  12781  hashdvds  12795  crth  12798  eulerthlemh  12805  prmdiveq  12810  hashgcdlem  12812  hashgcdeq  12814  nnnn0modprm0  12830  pclemub  12862  pceu  12870  pcmul  12876  pcqmul  12878  pcgcd1  12903  pc2dvds  12905  difsqpwdvds  12913  pcmpt  12918  prmpwdvds  12930  1arith  12942  mul4sq  12969  4sqlemafi  12970  4sqlemffi  12971  4sqexercise2  12974  ennnfonelemg  13026  ennnfonelemex  13037  ennnfonelemrnh  13039  ennnfonelemf1  13041  ennnfonelemrn  13042  ennnfonelemdm  13043  ennnfonelemim  13047  ennnfone  13048  ctinf  13053  ctiunctlemfo  13062  nninfdclemcl  13071  nninfdclemf  13072  nninfdclemp1  13073  unbendc  13077  isstruct2r  13095  setscom  13124  ercpbl  13416  opifismgmdc  13456  grpinvalem  13470  igsumvalx  13474  gsumfzval  13476  gsumval2  13482  sgrppropd  13498  prdssgrpd  13500  mndpropd  13525  issubmnd  13527  submnd0  13529  prdsmndd  13533  mhmf1o  13555  subsubm  13568  0mhm  13571  resmhm  13572  mhmco  13575  mhmima  13576  mhmeql  13577  gsumfzz  13580  gsumwsubmcl  13581  gsumfzcl  13584  grprcan  13622  grpinvid1  13637  grpinvid2  13638  grplcan  13647  grplmulf1o  13659  grpnpncan0  13681  dfgrp3mlem  13683  grplactcnv  13687  pwssub  13698  mulgval  13711  mulgfng  13713  mulgnngsum  13716  mulg1  13718  mulgnnp1  13719  mulgneg  13729  mulgnndir  13740  mulgdirlem  13742  mulgnn0ass  13747  mulgass  13748  subgmulg  13777  issubg4m  13782  subsubg  13786  subgintm  13787  isnsg3  13796  eqgcpbl  13817  ghmeql  13856  ghmnsgima  13857  ghmnsgpreima  13858  ghmf1  13862  ghmf1o  13864  conjghm  13865  qusghm  13871  ablpncan3  13906  invghm  13918  eqgabl  13919  gsumfzreidx  13926  gsumfzsubmcl  13927  gsumfzmptfidmadd  13928  gsumfzmhm  13932  rngpropd  13971  imasrng  13972  qusrng  13974  srglmhm  14009  srgrmhm  14010  ringpropd  14054  ringlghm  14077  ringrghm  14078  imasring  14080  qusring2  14082  opprrngbg  14094  dvdsrvald  14110  dvdsrd  14111  dvdsrex  14115  dvdsrtr  14118  unitpropdg  14165  rhmopp  14193  isnzr2  14201  issubrng2  14227  subrngintm  14229  subsubrng  14231  subrgintm  14260  subsubrg  14262  rhmpropd  14271  aprap  14303  lmodprop2d  14365  rmodislmod  14368  lssvacl  14382  lssvsubcl  14383  lssvscl  14392  islss3  14396  lss1d  14400  rnglidlmcl  14497  2idlcpblrng  14540  crngridl  14547  expghmap  14624  mulgghm2  14625  mulgrhm  14626  znf1o  14668  znleval  14670  znidom  14674  znidomb  14675  znunit  14676  mplsubgfilemcl  14716  iuncld  14842  ssnei2  14884  topssnei  14889  restopnb  14908  cnfval  14921  cnpfval  14922  iscnp4  14945  cnptopco  14949  cncnpi  14955  cncnp  14957  cnconst2  14960  cnrest2  14963  cnptoprest  14966  cnptoprest2  14967  cnpdis  14969  lmss  14973  lmtopcnp  14977  neitx  14995  txcnp  14998  txrest  15003  txdis1cn  15005  txlm  15006  cnmpt21  15018  imasnopn  15026  xmetres2  15106  blvalps  15115  blval  15116  elbl2ps  15119  elbl2  15120  blhalf  15135  blssexps  15156  blssex  15157  ssblex  15158  blin2  15159  bdmetval  15227  xmetxp  15234  xmettx  15237  metcnpi3  15244  txmetcnp  15245  addcncntoplem  15288  fsumcncntop  15294  elcncf2  15301  mulc1cncf  15316  cncfco  15318  cncfmet  15319  cncfmptc  15323  mulcncf  15335  dedekindeulemub  15345  dedekindeulemloc  15346  dedekindeulemlu  15348  dedekindeu  15350  dedekindicclemub  15354  dedekindicclemloc  15355  dedekindicclemlu  15357  dedekindicclemicc  15359  dedekindicc  15360  ivthinclemlopn  15363  ivthinclemuopn  15365  dich0  15379  limcimo  15392  cnplimccntop  15397  limccnp2lem  15403  limccnp2cntop  15404  dvfvalap  15408  dveflem  15453  plycolemc  15485  plyco  15486  plyrecj  15490  reeff1olem  15498  reeff1oleme  15499  eflt  15502  sin0pilem2  15509  pilem3  15510  ioocosf1o  15581  cxplt  15643  cxple  15644  cxplt3  15647  apcxp2  15666  rprelogbmul  15682  rprelogbdiv  15684  logbgt0b  15693  logbgcd1irrap  15697  mpodvdsmulf1o  15717  fsumdvdsmul  15718  lgsdir2lem5  15764  lgsdi  15769  lgsne0  15770  gausslemma2dlem1f1o  15792  lgseisenlem2  15803  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad2lem2  15814  lgsquad2  15815  2sqlem6  15852  2sqlem8  15855  2sqlem9  15856  2sqlem10  15857  upgredg  15998  usgredg4  16069  uspgredg2vlem  16074  usgr1eop  16099  upgrspanop  16137  umgrspanop  16138  usgrspanop  16139  vtxedgfi  16143  vtxlpfi  16144  iswlkg  16183  upgriswlkdc  16214  upgr2wlkdc  16231  clwwlkccatlem  16254  clwwlknonex2e  16294  nnti  16612  pwtrufal  16619  pwf1oexmid  16621  sssneq  16624  qdencn  16652  cvgcmp2n  16658  trilpolemlt1  16666  trirec0  16669  redc0  16682  reap0  16683  cndcap  16684  nconstwlpolemgt0  16689  neap0mkv  16694  supfz  16696  inffz  16697  gfsumval  16701  gfsumcl  16708