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  990  simp1rr  1090  simp2rr  1094  simp3rr  1098  elpr2elpr  3879  invdisjrab  4102  disjiun  4103  reg2exmidlema  4655  reg3exmidlemwe  4700  nnsucpred  4738  iotam  5343  fvmptt  5768  fcof1  5955  fliftfun  5968  isotr  5988  riotass2  6031  acexmidlemab  6043  ovmpodf  6184  fnmpoovd  6410  1stconst  6416  2ndconst  6417  cnvf1olem  6419  f1od2  6430  suppcofn  6465  smoiso  6532  tfrcldm  6593  tfrcl  6594  nntr2  6735  swoer  6794  erinxp  6842  ecopovsymg  6867  th3qlem1  6870  f1imaen2g  7032  pw2f1odclem  7086  mapdom1g  7099  fict  7122  fidifsnen  7124  dif1enen  7136  fiunsnnn  7137  fisbth  7139  findcard2d  7147  findcard2sd  7148  diffifi  7150  ac6sfi  7154  fimax2gtri  7158  nnwetri  7175  unsnfi  7178  unsnfidcex  7179  unsnfidcel  7180  fisseneq  7194  ssfirab  7196  exmidssfi  7198  fidcenumlemrk  7223  fidcenumlemr  7224  sbthlemi6  7231  sbthlemi8  7233  isbth  7236  fiuni  7264  supmaxti  7294  infminti  7317  ordiso2  7325  eldju2ndl  7362  eldju2ndr  7363  omp1eomlem  7384  difinfsnlem  7389  difinfinf  7391  ctmlemr  7398  ctssdccl  7401  nninfninc  7413  fodjum  7436  fodju0  7437  omniwomnimkv  7457  exmidfodomrlemrALT  7505  acfun  7513  exmidaclem  7514  netap  7564  exmidmotap  7571  ccfunen  7574  cc1  7575  cc2lem  7576  dfplpq2  7665  dfmpq2  7666  mulpipqqs  7684  distrnqg  7698  enq0sym  7743  enq0tr  7745  distrnq0  7770  prarloclem3  7808  genplt2i  7821  addlocpr  7847  prmuloc  7877  distrlem1prl  7893  distrlem1pru  7894  ltexprlemopl  7912  ltexprlemopu  7914  ltexprlemfl  7920  ltexprlemrl  7921  ltexprlemfu  7922  ltexprlemru  7923  addcanprleml  7925  addcanprlemu  7926  ltaprg  7930  prplnqu  7931  addextpr  7932  recexprlemdisj  7941  recexprlemloc  7942  aptiprleml  7950  aptiprlemu  7951  ltmprr  7953  archpr  7954  cauappcvgprlemopl  7957  cauappcvgprlemopu  7959  cauappcvgprlemdisj  7962  cauappcvgprlemloc  7963  cauappcvgprlem1  7970  cauappcvgprlemlim  7972  caucvgprlemnkj  7977  caucvgprlemopl  7980  caucvgprlemopu  7982  caucvgprlemdisj  7985  caucvgprlemloc  7986  caucvgprprlemnkltj  8000  caucvgprprlemnkeqj  8001  caucvgprprlemnjltk  8002  caucvgprprlemml  8005  caucvgprprlemmu  8006  caucvgprprlemopl  8008  caucvgprprlemopu  8010  caucvgprprlemdisj  8013  caucvgprprlemloc  8014  caucvgprprlemaddq  8019  suplocexprlemrl  8028  suplocexprlemmu  8029  suplocexprlemru  8030  suplocexprlemdisj  8031  suplocexprlemloc  8032  suplocexprlemex  8033  suplocexprlemub  8034  recexgt0sr  8084  mulgt0sr  8089  prsrriota  8099  suplocsrlem  8119  addcnsr  8145  mulcnsr  8146  mulcnsrec  8154  axmulcom  8182  rereceu  8200  axarch  8202  axcaucvglemres  8210  axpre-suploclemres  8212  lelttr  8358  ltletr  8359  addcan  8449  addcan2  8450  addsub4  8512  ltadd2  8689  le2add  8714  lt2add  8715  lt2sub  8730  le2sub  8731  eqord1  8753  rereim  8856  apreap  8857  apreim  8873  mulreim  8874  apcotr  8877  apadd1  8878  addext  8880  apneg  8881  mulext1  8882  mulext  8884  ltleap  8902  aprcl  8916  mulap0  8924  mulcanapd  8931  recapb  8941  rec11ap  8980  rec11rap  8981  divdivdivap  8983  ddcanap  8996  divadddivap  8997  prodgt0gt0  9121  prodgt0  9122  prodge0  9124  lemulge11  9136  lt2mul2div  9149  ltrec  9153  lerec  9154  lerec2  9159  ledivp1  9173  mulle0r  9214  nn0ge0div  9661  suprzclex  9672  qapne  9967  xrlelttr  10135  xrltletr  10136  xrre3  10151  xrrege0  10154  xaddge0  10207  xle2add  10208  xlt2add  10209  fzass4  10392  fzrev  10414  elfz1b  10420  eluzgtdifelfzo  10538  fzocatel  10540  zsupcllemstep  10585  zsupcllemex  10586  zssinfcl  10588  suprzubdc  10592  exbtwnzlemex  10605  rebtwn2z  10610  modqid  10707  modqcyc  10717  modqaddabs  10720  modqaddmod  10721  mulqaddmodid  10722  modqadd2mod  10732  modqltm1p1mod  10734  modqsubmod  10740  modqsubmodmod  10741  modaddmodup  10745  modqmulmod  10747  modqmulmodr  10748  modqaddmulmod  10749  modqsubdir  10751  frec2uzisod  10765  uzennn  10794  iseqovex  10816  seqvalcd  10819  seq1g  10821  seqf  10822  seqovcd  10825  seqclg  10830  seqm1g  10832  seq3shft2  10839  seqshft2g  10840  monoord  10843  iseqf1olemnab  10859  seqf1oglem1  10877  seqf1og  10879  seqhomog  10888  seqfeq4g  10889  seq3distr  10890  expnegzap  10931  ltexp2a  10949  le2sq2  10973  bernneq  11018  expnlbnd2  11023  nn0ltexp2  11067  nn0opth2  11082  faclbnd  11099  bcval5  11121  hashcl  11139  hashen  11142  fihashdom  11162  hashunlem  11163  hashun  11164  hashxp  11186  fimaxq  11187  sseqn  11196  hashfibclem  11199  hashfibc  11200  zfz1isolem1  11205  zfz1iso  11206  seq3coll  11207  sswrd  11226  ccatw2s1p1g  11326  ccatw2s1p2  11327  ccat2s1fstg  11329  wrdind  11407  pfxccatin12lem1  11413  pfxccatin12lem3  11417  reuccatpfxs1lem  11431  cvg1nlemres  11663  cvg1n  11664  resqrexlemp1rp  11684  resqrexlemoverl  11699  resqrexlemex  11703  sqrtsq  11722  abslt  11766  absle  11767  abs3lem  11789  maxleastlt  11893  maxltsup  11896  fimaxre2  11905  negfi  11906  xrmaxleastlt  11934  xrmaxltsup  11936  xrmaxaddlem  11938  2clim  11979  climcn2  11987  addcn2  11988  mulcn2  11990  reccn2ap  11991  climge0  12003  climcau  12025  fzf1o  12054  summodclem2  12061  summodc  12062  zsumdc  12063  fsumf1o  12069  fisumss  12071  fsum3cvg3  12075  fsumcl2lem  12077  fsumadd  12085  mptfzshft  12121  fsumrev  12122  fsummulc2  12127  fsumconst  12133  modfsummod  12137  fsumrelem  12150  binom  12163  cvgratnn  12210  mertenslemub  12213  prodmodclem2  12256  prodmodc  12257  zproddc  12258  fprodf1o  12267  fprodssdc  12269  fprodmul  12270  fprodcl2lem  12284  fprodrev  12298  fprodconst  12299  fprodap0  12300  fprodrec  12308  fprodap0f  12315  fprodle  12319  fprodmodd  12320  efcllem  12338  tanaddaplem  12417  moddvds  12478  dvdsflip  12530  oexpneg  12556  nn0o  12586  fldivndvdslt  12616  bitsfi  12636  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlemeu  12696  dfgcd3  12699  dfgcd2  12703  dvdsmulgcd  12714  bezoutr  12721  nninfctlemfo  12729  lcmgcdlem  12767  coprmdvds2  12783  qredeu  12787  rpdvds  12789  cncongr1  12793  prmind2  12810  isprm5lem  12831  isprm6  12837  oddpwdclemdc  12863  nonsq  12897  hashdvds  12911  crth  12914  eulerthlemh  12921  prmdiveq  12926  hashgcdlem  12928  hashgcdeq  12930  nnnn0modprm0  12946  pclemub  12978  pceu  12986  pcmul  12992  pcqmul  12994  pcgcd1  13019  pc2dvds  13021  difsqpwdvds  13029  pcmpt  13034  prmpwdvds  13046  1arith  13058  mul4sq  13085  4sqlemafi  13086  4sqlemffi  13087  4sqexercise2  13090  ennnfonelemg  13143  ennnfonelemex  13154  ennnfonelemrnh  13156  ennnfonelemf1  13158  ennnfonelemrn  13159  ennnfonelemdm  13160  ennnfonelemim  13164  ennnfone  13165  ctinf  13170  ctiunctlemfo  13179  nninfdclemcl  13188  nninfdclemf  13189  nninfdclemp1  13190  unbendc  13194  isstruct2r  13212  setscom  13241  ercpbl  13533  opifismgmdc  13573  grpinvalem  13587  igsumvalx  13591  gsumfzval  13593  gsumval2  13599  sgrppropd  13615  prdssgrpd  13617  mndpropd  13642  issubmnd  13644  submnd0  13646  prdsmndd  13650  mhmf1o  13672  subsubm  13685  0mhm  13688  resmhm  13689  mhmco  13692  mhmima  13693  mhmeql  13694  gsumfzz  13697  gsumwsubmcl  13698  gsumfzcl  13701  grprcan  13739  grpinvid1  13754  grpinvid2  13755  grplcan  13764  grplmulf1o  13776  grpnpncan0  13798  dfgrp3mlem  13800  grplactcnv  13804  pwssub  13815  mulgval  13828  mulgfng  13830  mulgnngsum  13833  mulg1  13835  mulgnnp1  13836  mulgneg  13846  mulgnndir  13857  mulgdirlem  13859  mulgnn0ass  13864  mulgass  13865  subgmulg  13894  issubg4m  13899  subsubg  13903  subgintm  13904  isnsg3  13913  eqgcpbl  13934  ghmeql  13973  ghmnsgima  13974  ghmnsgpreima  13975  ghmf1  13979  ghmf1o  13981  conjghm  13982  qusghm  13988  ablpncan3  14023  invghm  14035  eqgabl  14036  gsumfzreidx  14043  gsumfzsubmcl  14044  gsumfzmptfidmadd  14045  gsumfzmhm  14049  rngpropd  14088  imasrng  14089  qusrng  14091  srglmhm  14126  srgrmhm  14127  ringpropd  14171  ringlghm  14194  ringrghm  14195  imasring  14197  qusring2  14199  opprrngbg  14211  dvdsrvald  14227  dvdsrd  14228  dvdsrex  14232  dvdsrtr  14235  unitpropdg  14282  rhmopp  14310  isnzr2  14318  issubrng2  14344  subrngintm  14346  subsubrng  14348  subrgintm  14377  subsubrg  14379  rhmpropd  14388  aprap  14421  lmodprop2d  14483  rmodislmod  14486  lssvacl  14500  lssvsubcl  14501  lssvscl  14510  islss3  14514  lss1d  14518  rnglidlmcl  14615  2idlcpblrng  14658  crngridl  14665  expghmap  14742  mulgghm2  14743  mulgrhm  14744  znf1o  14786  znleval  14788  znidom  14792  znidomb  14793  znunit  14794  psrbagcon  14813  mplsubgfilemcl  14841  iuncld  14967  ssnei2  15009  topssnei  15014  restopnb  15033  cnfval  15046  cnpfval  15047  iscnp4  15070  cnptopco  15074  cncnpi  15080  cncnp  15082  cnconst2  15085  cnrest2  15088  cnptoprest  15091  cnptoprest2  15092  cnpdis  15094  lmss  15098  lmtopcnp  15102  neitx  15120  txcnp  15123  txrest  15128  txdis1cn  15130  txlm  15131  cnmpt21  15143  imasnopn  15151  xmetres2  15231  blvalps  15240  blval  15241  elbl2ps  15244  elbl2  15245  blhalf  15260  blssexps  15281  blssex  15282  ssblex  15283  blin2  15284  bdmetval  15352  xmetxp  15359  xmettx  15362  metcnpi3  15369  txmetcnp  15370  addcncntoplem  15413  fsumcncntop  15419  elcncf2  15426  mulc1cncf  15441  cncfco  15443  cncfmet  15444  cncfmptc  15448  mulcncf  15460  dedekindeulemub  15470  dedekindeulemloc  15471  dedekindeulemlu  15473  dedekindeu  15475  dedekindicclemub  15479  dedekindicclemloc  15480  dedekindicclemlu  15482  dedekindicclemicc  15484  dedekindicc  15485  ivthinclemlopn  15488  ivthinclemuopn  15490  dich0  15504  limcimo  15517  cnplimccntop  15522  limccnp2lem  15528  limccnp2cntop  15529  dvfvalap  15533  dveflem  15578  plycolemc  15610  plyco  15611  plyrecj  15615  reeff1olem  15623  reeff1oleme  15624  eflt  15627  sin0pilem2  15634  pilem3  15635  ioocosf1o  15706  cxplt  15768  cxple  15769  cxplt3  15772  apcxp2  15791  rprelogbmul  15807  rprelogbdiv  15809  logbgt0b  15818  logbgcd1irrap  15822  pellexlem3  15834  mpodvdsmulf1o  15845  fsumdvdsmul  15846  lgsdir2lem5  15892  lgsdi  15897  lgsne0  15898  gausslemma2dlem1f1o  15920  lgseisenlem2  15931  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad2lem2  15942  lgsquad2  15943  2sqlem6  15980  2sqlem8  15983  2sqlem9  15984  2sqlem10  15985  upgredg  16126  usgredg4  16197  uspgredg2vlem  16202  usgr1eop  16227  upgrspanop  16265  umgrspanop  16266  usgrspanop  16267  vtxedgfi  16271  vtxlpfi  16272  iswlkg  16311  upgriswlkdc  16342  upgr2wlkdc  16359  clwwlkccatlem  16382  clwwlknonex2e  16422  nnti  16753  pwtrufal  16758  pwf1oexmid  16760  sssneq  16763  qdencn  16794  cvgcmp2n  16804  trilpolemlt1  16812  trirec0  16815  qdiff  16820  redc0  16829  reap0  16830  cndcap  16831  nconstwlpolemgt0  16836  neap0mkv  16841  supfz  16843  inffz  16844  gfsumval  16848  gfsumz  16855  gfsumcl  16856