Theorem simprr 531

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprr	|- ( ( ph /\ ( ps /\ ch ) ) -> ch )

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2	1	ad2antll 491	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ch )

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  4038  reg2exmidlema  4580  reg3exmidlemwe  4625  nnsucpred  4663  iotam  5260  fvmptt  5665  fcof1  5842  fliftfun  5855  isotr  5875  riotass2  5916  acexmidlemab  5928  ovmpodf  6067  fnmpoovd  6291  1stconst  6297  2ndconst  6298  cnvf1olem  6300  f1od2  6311  smoiso  6378  tfrcldm  6439  tfrcl  6440  nntr2  6579  swoer  6638  erinxp  6686  ecopovsymg  6711  th3qlem1  6714  f1imaen2g  6870  pw2f1odclem  6913  mapdom1g  6926  fict  6947  fidifsnen  6949  dif1enen  6959  fiunsnnn  6960  fisbth  6962  findcard2d  6970  findcard2sd  6971  diffifi  6973  ac6sfi  6977  fimax2gtri  6980  nnwetri  6995  unsnfi  6998  unsnfidcex  6999  unsnfidcel  7000  fisseneq  7013  ssfirab  7015  fidcenumlemrk  7038  fidcenumlemr  7039  sbthlemi6  7046  sbthlemi8  7048  isbth  7051  fiuni  7062  supmaxti  7088  infminti  7111  ordiso2  7119  eldju2ndl  7156  eldju2ndr  7157  omp1eomlem  7178  difinfsnlem  7183  difinfinf  7185  ctmlemr  7192  ctssdccl  7195  nninfninc  7207  fodjum  7230  fodju0  7231  omniwomnimkv  7251  exmidfodomrlemrALT  7293  acfun  7301  exmidaclem  7302  netap  7348  exmidmotap  7355  ccfunen  7358  cc1  7359  cc2lem  7360  dfplpq2  7449  dfmpq2  7450  mulpipqqs  7468  distrnqg  7482  enq0sym  7527  enq0tr  7529  distrnq0  7554  prarloclem3  7592  genplt2i  7605  addlocpr  7631  prmuloc  7661  distrlem1prl  7677  distrlem1pru  7678  ltexprlemopl  7696  ltexprlemopu  7698  ltexprlemfl  7704  ltexprlemrl  7705  ltexprlemfu  7706  ltexprlemru  7707  addcanprleml  7709  addcanprlemu  7710  ltaprg  7714  prplnqu  7715  addextpr  7716  recexprlemdisj  7725  recexprlemloc  7726  aptiprleml  7734  aptiprlemu  7735  ltmprr  7737  archpr  7738  cauappcvgprlemopl  7741  cauappcvgprlemopu  7743  cauappcvgprlemdisj  7746  cauappcvgprlemloc  7747  cauappcvgprlem1  7754  cauappcvgprlemlim  7756  caucvgprlemnkj  7761  caucvgprlemopl  7764  caucvgprlemopu  7766  caucvgprlemdisj  7769  caucvgprlemloc  7770  caucvgprprlemnkltj  7784  caucvgprprlemnkeqj  7785  caucvgprprlemnjltk  7786  caucvgprprlemml  7789  caucvgprprlemmu  7790  caucvgprprlemopl  7792  caucvgprprlemopu  7794  caucvgprprlemdisj  7797  caucvgprprlemloc  7798  caucvgprprlemaddq  7803  suplocexprlemrl  7812  suplocexprlemmu  7813  suplocexprlemru  7814  suplocexprlemdisj  7815  suplocexprlemloc  7816  suplocexprlemex  7817  suplocexprlemub  7818  recexgt0sr  7868  mulgt0sr  7873  prsrriota  7883  suplocsrlem  7903  addcnsr  7929  mulcnsr  7930  mulcnsrec  7938  axmulcom  7966  rereceu  7984  axarch  7986  axcaucvglemres  7994  axpre-suploclemres  7996  lelttr  8143  ltletr  8144  addcan  8234  addcan2  8235  addsub4  8297  ltadd2  8474  le2add  8499  lt2add  8500  lt2sub  8515  le2sub  8516  eqord1  8538  rereim  8641  apreap  8642  apreim  8658  mulreim  8659  apcotr  8662  apadd1  8663  addext  8665  apneg  8666  mulext1  8667  mulext  8669  ltleap  8687  aprcl  8701  mulap0  8709  mulcanapd  8716  recapb  8726  rec11ap  8765  rec11rap  8766  divdivdivap  8768  ddcanap  8781  divadddivap  8782  prodgt0gt0  8906  prodgt0  8907  prodge0  8909  lemulge11  8921  lt2mul2div  8934  ltrec  8938  lerec  8939  lerec2  8944  ledivp1  8958  mulle0r  8999  nn0ge0div  9442  suprzclex  9453  qapne  9742  xrlelttr  9910  xrltletr  9911  xrre3  9926  xrrege0  9929  xaddge0  9982  xle2add  9983  xlt2add  9984  fzass4  10166  fzrev  10188  elfz1b  10194  eluzgtdifelfzo  10307  fzocatel  10309  zsupcllemstep  10353  zsupcllemex  10354  zssinfcl  10356  suprzubdc  10360  exbtwnzlemex  10373  rebtwn2z  10378  modqid  10475  modqcyc  10485  modqaddabs  10488  modqaddmod  10489  mulqaddmodid  10490  modqadd2mod  10500  modqltm1p1mod  10502  modqsubmod  10508  modqsubmodmod  10509  modaddmodup  10513  modqmulmod  10515  modqmulmodr  10516  modqaddmulmod  10517  modqsubdir  10519  frec2uzisod  10533  uzennn  10562  iseqovex  10584  seqvalcd  10587  seq1g  10589  seqf  10590  seqovcd  10593  seqclg  10598  seqm1g  10600  seq3shft2  10607  seqshft2g  10608  monoord  10611  iseqf1olemnab  10627  seqf1oglem1  10645  seqf1og  10647  seqhomog  10656  seqfeq4g  10657  seq3distr  10658  expnegzap  10699  ltexp2a  10717  le2sq2  10741  bernneq  10786  expnlbnd2  10791  nn0ltexp2  10835  nn0opth2  10850  faclbnd  10867  bcval5  10889  hashcl  10907  hashen  10910  fihashdom  10929  hashunlem  10930  hashun  10931  hashxp  10952  fimaxq  10953  zfz1isolem1  10966  zfz1iso  10967  seq3coll  10968  sswrd  10978  cvg1nlemres  11215  cvg1n  11216  resqrexlemp1rp  11236  resqrexlemoverl  11251  resqrexlemex  11255  sqrtsq  11274  abslt  11318  absle  11319  abs3lem  11341  maxleastlt  11445  maxltsup  11448  fimaxre2  11457  negfi  11458  xrmaxleastlt  11486  xrmaxltsup  11488  xrmaxaddlem  11490  2clim  11531  climcn2  11539  addcn2  11540  mulcn2  11542  reccn2ap  11543  climge0  11555  climcau  11577  summodclem2  11612  summodc  11613  zsumdc  11614  fsumf1o  11620  fisumss  11622  fsum3cvg3  11626  fsumcl2lem  11628  fsumadd  11636  mptfzshft  11672  fsumrev  11673  fsummulc2  11678  fsumconst  11684  modfsummod  11688  fsumrelem  11701  binom  11714  cvgratnn  11761  mertenslemub  11764  prodmodclem2  11807  prodmodc  11808  zproddc  11809  fprodf1o  11818  fprodssdc  11820  fprodmul  11821  fprodcl2lem  11835  fprodrev  11849  fprodconst  11850  fprodap0  11851  fprodrec  11859  fprodap0f  11866  fprodle  11870  fprodmodd  11871  efcllem  11889  tanaddaplem  11968  moddvds  12029  dvdsflip  12081  oexpneg  12107  nn0o  12137  fldivndvdslt  12167  bitsfi  12187  bezoutlemnewy  12236  bezoutlemstep  12237  bezoutlemeu  12247  dfgcd3  12250  dfgcd2  12254  dvdsmulgcd  12265  bezoutr  12272  nninfctlemfo  12280  lcmgcdlem  12318  coprmdvds2  12334  qredeu  12338  rpdvds  12340  cncongr1  12344  prmind2  12361  isprm5lem  12382  isprm6  12388  oddpwdclemdc  12414  nonsq  12448  hashdvds  12462  crth  12465  eulerthlemh  12472  prmdiveq  12477  hashgcdlem  12479  hashgcdeq  12481  nnnn0modprm0  12497  pclemub  12529  pceu  12537  pcmul  12543  pcqmul  12545  pcgcd1  12570  pc2dvds  12572  difsqpwdvds  12580  pcmpt  12585  prmpwdvds  12597  1arith  12609  mul4sq  12636  4sqlemafi  12637  4sqlemffi  12638  4sqexercise2  12641  ennnfonelemg  12693  ennnfonelemex  12704  ennnfonelemrnh  12706  ennnfonelemf1  12708  ennnfonelemrn  12709  ennnfonelemdm  12710  ennnfonelemim  12714  ennnfone  12715  ctinf  12720  ctiunctlemfo  12729  nninfdclemcl  12738  nninfdclemf  12739  nninfdclemp1  12740  unbendc  12744  isstruct2r  12762  setscom  12791  ercpbl  13081  opifismgmdc  13121  grpinvalem  13135  igsumvalx  13139  gsumfzval  13141  gsumval2  13147  sgrppropd  13163  prdssgrpd  13165  mndpropd  13190  issubmnd  13192  submnd0  13194  prdsmndd  13198  mhmf1o  13220  subsubm  13233  0mhm  13236  resmhm  13237  mhmco  13240  mhmima  13241  mhmeql  13242  gsumfzz  13245  gsumwsubmcl  13246  gsumfzcl  13249  grprcan  13287  grpinvid1  13302  grpinvid2  13303  grplcan  13312  grplmulf1o  13324  grpnpncan0  13346  dfgrp3mlem  13348  grplactcnv  13352  pwssub  13363  mulgval  13376  mulgfng  13378  mulgnngsum  13381  mulg1  13383  mulgnnp1  13384  mulgneg  13394  mulgnndir  13405  mulgdirlem  13407  mulgnn0ass  13412  mulgass  13413  subgmulg  13442  issubg4m  13447  subsubg  13451  subgintm  13452  isnsg3  13461  eqgcpbl  13482  ghmeql  13521  ghmnsgima  13522  ghmnsgpreima  13523  ghmf1  13527  ghmf1o  13529  conjghm  13530  qusghm  13536  ablpncan3  13571  invghm  13583  eqgabl  13584  gsumfzreidx  13591  gsumfzsubmcl  13592  gsumfzmptfidmadd  13593  gsumfzmhm  13597  rngpropd  13635  imasrng  13636  qusrng  13638  srglmhm  13673  srgrmhm  13674  ringpropd  13718  ringlghm  13741  ringrghm  13742  imasring  13744  qusring2  13746  opprrngbg  13758  dvdsrvald  13773  dvdsrd  13774  dvdsrex  13778  dvdsrtr  13781  unitpropdg  13828  rhmopp  13856  isnzr2  13864  issubrng2  13890  subrngintm  13892  subsubrng  13894  subrgintm  13923  subsubrg  13925  rhmpropd  13934  aprap  13966  lmodprop2d  14028  rmodislmod  14031  lssvacl  14045  lssvsubcl  14046  lssvscl  14055  islss3  14059  lss1d  14063  rnglidlmcl  14160  2idlcpblrng  14203  crngridl  14210  expghmap  14287  mulgghm2  14288  mulgrhm  14289  znf1o  14331  znleval  14333  znidom  14337  znidomb  14338  znunit  14339  mplsubgfilemcl  14379  iuncld  14505  ssnei2  14547  topssnei  14552  restopnb  14571  cnfval  14584  cnpfval  14585  iscnp4  14608  cnptopco  14612  cncnpi  14618  cncnp  14620  cnconst2  14623  cnrest2  14626  cnptoprest  14629  cnptoprest2  14630  cnpdis  14632  lmss  14636  lmtopcnp  14640  neitx  14658  txcnp  14661  txrest  14666  txdis1cn  14668  txlm  14669  cnmpt21  14681  imasnopn  14689  xmetres2  14769  blvalps  14778  blval  14779  elbl2ps  14782  elbl2  14783  blhalf  14798  blssexps  14819  blssex  14820  ssblex  14821  blin2  14822  bdmetval  14890  xmetxp  14897  xmettx  14900  metcnpi3  14907  txmetcnp  14908  addcncntoplem  14951  fsumcncntop  14957  elcncf2  14964  mulc1cncf  14979  cncfco  14981  cncfmet  14982  cncfmptc  14986  mulcncf  14998  dedekindeulemub  15008  dedekindeulemloc  15009  dedekindeulemlu  15011  dedekindeu  15013  dedekindicclemub  15017  dedekindicclemloc  15018  dedekindicclemlu  15020  dedekindicclemicc  15022  dedekindicc  15023  ivthinclemlopn  15026  ivthinclemuopn  15028  dich0  15042  limcimo  15055  cnplimccntop  15060  limccnp2lem  15066  limccnp2cntop  15067  dvfvalap  15071  dveflem  15116  plycolemc  15148  plyco  15149  plyrecj  15153  reeff1olem  15161  reeff1oleme  15162  eflt  15165  sin0pilem2  15172  pilem3  15173  ioocosf1o  15244  cxplt  15306  cxple  15307  cxplt3  15310  apcxp2  15329  rprelogbmul  15345  rprelogbdiv  15347  logbgt0b  15356  logbgcd1irrap  15360  mpodvdsmulf1o  15380  fsumdvdsmul  15381  lgsdir2lem5  15427  lgsdi  15432  lgsne0  15433  gausslemma2dlem1f1o  15455  lgseisenlem2  15466  lgsquadlem1  15472  lgsquadlem2  15473  lgsquadlem3  15474  lgsquad2lem2  15477  lgsquad2  15478  2sqlem6  15515  2sqlem8  15518  2sqlem9  15519  2sqlem10  15520  nnti  15793  pwtrufal  15798  pwf1oexmid  15800  sssneq  15803  qdencn  15830  cvgcmp2n  15836  trilpolemlt1  15844  trirec0  15847  redc0  15860  reap0  15861  cndcap  15862  nconstwlpolemgt0  15867  neap0mkv  15872  supfz  15874  inffz  15875