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  4581  reg3exmidlemwe  4626  nnsucpred  4664  iotam  5262  fvmptt  5670  fcof1  5851  fliftfun  5864  isotr  5884  riotass2  5925  acexmidlemab  5937  ovmpodf  6076  fnmpoovd  6300  1stconst  6306  2ndconst  6307  cnvf1olem  6309  f1od2  6320  smoiso  6387  tfrcldm  6448  tfrcl  6449  nntr2  6588  swoer  6647  erinxp  6695  ecopovsymg  6720  th3qlem1  6723  f1imaen2g  6884  pw2f1odclem  6930  mapdom1g  6943  fict  6964  fidifsnen  6966  dif1enen  6976  fiunsnnn  6977  fisbth  6979  findcard2d  6987  findcard2sd  6988  diffifi  6990  ac6sfi  6994  fimax2gtri  6997  nnwetri  7012  unsnfi  7015  unsnfidcex  7016  unsnfidcel  7017  fisseneq  7030  ssfirab  7032  fidcenumlemrk  7055  fidcenumlemr  7056  sbthlemi6  7063  sbthlemi8  7065  isbth  7068  fiuni  7079  supmaxti  7105  infminti  7128  ordiso2  7136  eldju2ndl  7173  eldju2ndr  7174  omp1eomlem  7195  difinfsnlem  7200  difinfinf  7202  ctmlemr  7209  ctssdccl  7212  nninfninc  7224  fodjum  7247  fodju0  7248  omniwomnimkv  7268  exmidfodomrlemrALT  7310  acfun  7318  exmidaclem  7319  netap  7365  exmidmotap  7372  ccfunen  7375  cc1  7376  cc2lem  7377  dfplpq2  7466  dfmpq2  7467  mulpipqqs  7485  distrnqg  7499  enq0sym  7544  enq0tr  7546  distrnq0  7571  prarloclem3  7609  genplt2i  7622  addlocpr  7648  prmuloc  7678  distrlem1prl  7694  distrlem1pru  7695  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemfl  7721  ltexprlemrl  7722  ltexprlemfu  7723  ltexprlemru  7724  addcanprleml  7726  addcanprlemu  7727  ltaprg  7731  prplnqu  7732  addextpr  7733  recexprlemdisj  7742  recexprlemloc  7743  aptiprleml  7751  aptiprlemu  7752  ltmprr  7754  archpr  7755  cauappcvgprlemopl  7758  cauappcvgprlemopu  7760  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlem1  7771  cauappcvgprlemlim  7773  caucvgprlemnkj  7778  caucvgprlemopl  7781  caucvgprlemopu  7783  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemnjltk  7803  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemopu  7811  caucvgprprlemdisj  7814  caucvgprprlemloc  7815  caucvgprprlemaddq  7820  suplocexprlemrl  7829  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemex  7834  suplocexprlemub  7835  recexgt0sr  7885  mulgt0sr  7890  prsrriota  7900  suplocsrlem  7920  addcnsr  7946  mulcnsr  7947  mulcnsrec  7955  axmulcom  7983  rereceu  8001  axarch  8003  axcaucvglemres  8011  axpre-suploclemres  8013  lelttr  8160  ltletr  8161  addcan  8251  addcan2  8252  addsub4  8314  ltadd2  8491  le2add  8516  lt2add  8517  lt2sub  8532  le2sub  8533  eqord1  8555  rereim  8658  apreap  8659  apreim  8675  mulreim  8676  apcotr  8679  apadd1  8680  addext  8682  apneg  8683  mulext1  8684  mulext  8686  ltleap  8704  aprcl  8718  mulap0  8726  mulcanapd  8733  recapb  8743  rec11ap  8782  rec11rap  8783  divdivdivap  8785  ddcanap  8798  divadddivap  8799  prodgt0gt0  8923  prodgt0  8924  prodge0  8926  lemulge11  8938  lt2mul2div  8951  ltrec  8955  lerec  8956  lerec2  8961  ledivp1  8975  mulle0r  9016  nn0ge0div  9459  suprzclex  9470  qapne  9759  xrlelttr  9927  xrltletr  9928  xrre3  9943  xrrege0  9946  xaddge0  9999  xle2add  10000  xlt2add  10001  fzass4  10183  fzrev  10205  elfz1b  10211  eluzgtdifelfzo  10324  fzocatel  10326  zsupcllemstep  10370  zsupcllemex  10371  zssinfcl  10373  suprzubdc  10377  exbtwnzlemex  10390  rebtwn2z  10395  modqid  10492  modqcyc  10502  modqaddabs  10505  modqaddmod  10506  mulqaddmodid  10507  modqadd2mod  10517  modqltm1p1mod  10519  modqsubmod  10525  modqsubmodmod  10526  modaddmodup  10530  modqmulmod  10532  modqmulmodr  10533  modqaddmulmod  10534  modqsubdir  10536  frec2uzisod  10550  uzennn  10579  iseqovex  10601  seqvalcd  10604  seq1g  10606  seqf  10607  seqovcd  10610  seqclg  10615  seqm1g  10617  seq3shft2  10624  seqshft2g  10625  monoord  10628  iseqf1olemnab  10644  seqf1oglem1  10662  seqf1og  10664  seqhomog  10673  seqfeq4g  10674  seq3distr  10675  expnegzap  10716  ltexp2a  10734  le2sq2  10758  bernneq  10803  expnlbnd2  10808  nn0ltexp2  10852  nn0opth2  10867  faclbnd  10884  bcval5  10906  hashcl  10924  hashen  10927  fihashdom  10946  hashunlem  10947  hashun  10948  hashxp  10969  fimaxq  10970  zfz1isolem1  10983  zfz1iso  10984  seq3coll  10985  sswrd  11001  cvg1nlemres  11238  cvg1n  11239  resqrexlemp1rp  11259  resqrexlemoverl  11274  resqrexlemex  11278  sqrtsq  11297  abslt  11341  absle  11342  abs3lem  11364  maxleastlt  11468  maxltsup  11471  fimaxre2  11480  negfi  11481  xrmaxleastlt  11509  xrmaxltsup  11511  xrmaxaddlem  11513  2clim  11554  climcn2  11562  addcn2  11563  mulcn2  11565  reccn2ap  11566  climge0  11578  climcau  11600  summodclem2  11635  summodc  11636  zsumdc  11637  fsumf1o  11643  fisumss  11645  fsum3cvg3  11649  fsumcl2lem  11651  fsumadd  11659  mptfzshft  11695  fsumrev  11696  fsummulc2  11701  fsumconst  11707  modfsummod  11711  fsumrelem  11724  binom  11737  cvgratnn  11784  mertenslemub  11787  prodmodclem2  11830  prodmodc  11831  zproddc  11832  fprodf1o  11841  fprodssdc  11843  fprodmul  11844  fprodcl2lem  11858  fprodrev  11872  fprodconst  11873  fprodap0  11874  fprodrec  11882  fprodap0f  11889  fprodle  11893  fprodmodd  11894  efcllem  11912  tanaddaplem  11991  moddvds  12052  dvdsflip  12104  oexpneg  12130  nn0o  12160  fldivndvdslt  12190  bitsfi  12210  bezoutlemnewy  12259  bezoutlemstep  12260  bezoutlemeu  12270  dfgcd3  12273  dfgcd2  12277  dvdsmulgcd  12288  bezoutr  12295  nninfctlemfo  12303  lcmgcdlem  12341  coprmdvds2  12357  qredeu  12361  rpdvds  12363  cncongr1  12367  prmind2  12384  isprm5lem  12405  isprm6  12411  oddpwdclemdc  12437  nonsq  12471  hashdvds  12485  crth  12488  eulerthlemh  12495  prmdiveq  12500  hashgcdlem  12502  hashgcdeq  12504  nnnn0modprm0  12520  pclemub  12552  pceu  12560  pcmul  12566  pcqmul  12568  pcgcd1  12593  pc2dvds  12595  difsqpwdvds  12603  pcmpt  12608  prmpwdvds  12620  1arith  12632  mul4sq  12659  4sqlemafi  12660  4sqlemffi  12661  4sqexercise2  12664  ennnfonelemg  12716  ennnfonelemex  12727  ennnfonelemrnh  12729  ennnfonelemf1  12731  ennnfonelemrn  12732  ennnfonelemdm  12733  ennnfonelemim  12737  ennnfone  12738  ctinf  12743  ctiunctlemfo  12752  nninfdclemcl  12761  nninfdclemf  12762  nninfdclemp1  12763  unbendc  12767  isstruct2r  12785  setscom  12814  ercpbl  13105  opifismgmdc  13145  grpinvalem  13159  igsumvalx  13163  gsumfzval  13165  gsumval2  13171  sgrppropd  13187  prdssgrpd  13189  mndpropd  13214  issubmnd  13216  submnd0  13218  prdsmndd  13222  mhmf1o  13244  subsubm  13257  0mhm  13260  resmhm  13261  mhmco  13264  mhmima  13265  mhmeql  13266  gsumfzz  13269  gsumwsubmcl  13270  gsumfzcl  13273  grprcan  13311  grpinvid1  13326  grpinvid2  13327  grplcan  13336  grplmulf1o  13348  grpnpncan0  13370  dfgrp3mlem  13372  grplactcnv  13376  pwssub  13387  mulgval  13400  mulgfng  13402  mulgnngsum  13405  mulg1  13407  mulgnnp1  13408  mulgneg  13418  mulgnndir  13429  mulgdirlem  13431  mulgnn0ass  13436  mulgass  13437  subgmulg  13466  issubg4m  13471  subsubg  13475  subgintm  13476  isnsg3  13485  eqgcpbl  13506  ghmeql  13545  ghmnsgima  13546  ghmnsgpreima  13547  ghmf1  13551  ghmf1o  13553  conjghm  13554  qusghm  13560  ablpncan3  13595  invghm  13607  eqgabl  13608  gsumfzreidx  13615  gsumfzsubmcl  13616  gsumfzmptfidmadd  13617  gsumfzmhm  13621  rngpropd  13659  imasrng  13660  qusrng  13662  srglmhm  13697  srgrmhm  13698  ringpropd  13742  ringlghm  13765  ringrghm  13766  imasring  13768  qusring2  13770  opprrngbg  13782  dvdsrvald  13797  dvdsrd  13798  dvdsrex  13802  dvdsrtr  13805  unitpropdg  13852  rhmopp  13880  isnzr2  13888  issubrng2  13914  subrngintm  13916  subsubrng  13918  subrgintm  13947  subsubrg  13949  rhmpropd  13958  aprap  13990  lmodprop2d  14052  rmodislmod  14055  lssvacl  14069  lssvsubcl  14070  lssvscl  14079  islss3  14083  lss1d  14087  rnglidlmcl  14184  2idlcpblrng  14227  crngridl  14234  expghmap  14311  mulgghm2  14312  mulgrhm  14313  znf1o  14355  znleval  14357  znidom  14361  znidomb  14362  znunit  14363  mplsubgfilemcl  14403  iuncld  14529  ssnei2  14571  topssnei  14576  restopnb  14595  cnfval  14608  cnpfval  14609  iscnp4  14632  cnptopco  14636  cncnpi  14642  cncnp  14644  cnconst2  14647  cnrest2  14650  cnptoprest  14653  cnptoprest2  14654  cnpdis  14656  lmss  14660  lmtopcnp  14664  neitx  14682  txcnp  14685  txrest  14690  txdis1cn  14692  txlm  14693  cnmpt21  14705  imasnopn  14713  xmetres2  14793  blvalps  14802  blval  14803  elbl2ps  14806  elbl2  14807  blhalf  14822  blssexps  14843  blssex  14844  ssblex  14845  blin2  14846  bdmetval  14914  xmetxp  14921  xmettx  14924  metcnpi3  14931  txmetcnp  14932  addcncntoplem  14975  fsumcncntop  14981  elcncf2  14988  mulc1cncf  15003  cncfco  15005  cncfmet  15006  cncfmptc  15010  mulcncf  15022  dedekindeulemub  15032  dedekindeulemloc  15033  dedekindeulemlu  15035  dedekindeu  15037  dedekindicclemub  15041  dedekindicclemloc  15042  dedekindicclemlu  15044  dedekindicclemicc  15046  dedekindicc  15047  ivthinclemlopn  15050  ivthinclemuopn  15052  dich0  15066  limcimo  15079  cnplimccntop  15084  limccnp2lem  15090  limccnp2cntop  15091  dvfvalap  15095  dveflem  15140  plycolemc  15172  plyco  15173  plyrecj  15177  reeff1olem  15185  reeff1oleme  15186  eflt  15189  sin0pilem2  15196  pilem3  15197  ioocosf1o  15268  cxplt  15330  cxple  15331  cxplt3  15334  apcxp2  15353  rprelogbmul  15369  rprelogbdiv  15371  logbgt0b  15380  logbgcd1irrap  15384  mpodvdsmulf1o  15404  fsumdvdsmul  15405  lgsdir2lem5  15451  lgsdi  15456  lgsne0  15457  gausslemma2dlem1f1o  15479  lgseisenlem2  15490  lgsquadlem1  15496  lgsquadlem2  15497  lgsquadlem3  15498  lgsquad2lem2  15501  lgsquad2  15502  2sqlem6  15539  2sqlem8  15542  2sqlem9  15543  2sqlem10  15544  nnti  15862  pwtrufal  15867  pwf1oexmid  15869  sssneq  15872  qdencn  15899  cvgcmp2n  15905  trilpolemlt1  15913  trirec0  15916  redc0  15929  reap0  15930  cndcap  15931  nconstwlpolemgt0  15936  neap0mkv  15941  supfz  15943  inffz  15944