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  1066  simp2rr  1070  simp3rr  1074  invdisjrab  4045  disjiun  4046  reg2exmidlema  4590  reg3exmidlemwe  4635  nnsucpred  4673  iotam  5272  fvmptt  5684  fcof1  5865  fliftfun  5878  isotr  5898  riotass2  5939  acexmidlemab  5951  ovmpodf  6090  fnmpoovd  6314  1stconst  6320  2ndconst  6321  cnvf1olem  6323  f1od2  6334  smoiso  6401  tfrcldm  6462  tfrcl  6463  nntr2  6602  swoer  6661  erinxp  6709  ecopovsymg  6734  th3qlem1  6737  f1imaen2g  6898  pw2f1odclem  6946  mapdom1g  6959  fict  6980  fidifsnen  6982  dif1enen  6992  fiunsnnn  6993  fisbth  6995  findcard2d  7003  findcard2sd  7004  diffifi  7006  ac6sfi  7010  fimax2gtri  7013  nnwetri  7028  unsnfi  7031  unsnfidcex  7032  unsnfidcel  7033  fisseneq  7046  ssfirab  7048  fidcenumlemrk  7071  fidcenumlemr  7072  sbthlemi6  7079  sbthlemi8  7081  isbth  7084  fiuni  7095  supmaxti  7121  infminti  7144  ordiso2  7152  eldju2ndl  7189  eldju2ndr  7190  omp1eomlem  7211  difinfsnlem  7216  difinfinf  7218  ctmlemr  7225  ctssdccl  7228  nninfninc  7240  fodjum  7263  fodju0  7264  omniwomnimkv  7284  exmidfodomrlemrALT  7327  acfun  7335  exmidaclem  7336  netap  7386  exmidmotap  7393  ccfunen  7396  cc1  7397  cc2lem  7398  dfplpq2  7487  dfmpq2  7488  mulpipqqs  7506  distrnqg  7520  enq0sym  7565  enq0tr  7567  distrnq0  7592  prarloclem3  7630  genplt2i  7643  addlocpr  7669  prmuloc  7699  distrlem1prl  7715  distrlem1pru  7716  ltexprlemopl  7734  ltexprlemopu  7736  ltexprlemfl  7742  ltexprlemrl  7743  ltexprlemfu  7744  ltexprlemru  7745  addcanprleml  7747  addcanprlemu  7748  ltaprg  7752  prplnqu  7753  addextpr  7754  recexprlemdisj  7763  recexprlemloc  7764  aptiprleml  7772  aptiprlemu  7773  ltmprr  7775  archpr  7776  cauappcvgprlemopl  7779  cauappcvgprlemopu  7781  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlem1  7792  cauappcvgprlemlim  7794  caucvgprlemnkj  7799  caucvgprlemopl  7802  caucvgprlemopu  7804  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprprlemnkltj  7822  caucvgprprlemnkeqj  7823  caucvgprprlemnjltk  7824  caucvgprprlemml  7827  caucvgprprlemmu  7828  caucvgprprlemopl  7830  caucvgprprlemopu  7832  caucvgprprlemdisj  7835  caucvgprprlemloc  7836  caucvgprprlemaddq  7841  suplocexprlemrl  7850  suplocexprlemmu  7851  suplocexprlemru  7852  suplocexprlemdisj  7853  suplocexprlemloc  7854  suplocexprlemex  7855  suplocexprlemub  7856  recexgt0sr  7906  mulgt0sr  7911  prsrriota  7921  suplocsrlem  7941  addcnsr  7967  mulcnsr  7968  mulcnsrec  7976  axmulcom  8004  rereceu  8022  axarch  8024  axcaucvglemres  8032  axpre-suploclemres  8034  lelttr  8181  ltletr  8182  addcan  8272  addcan2  8273  addsub4  8335  ltadd2  8512  le2add  8537  lt2add  8538  lt2sub  8553  le2sub  8554  eqord1  8576  rereim  8679  apreap  8680  apreim  8696  mulreim  8697  apcotr  8700  apadd1  8701  addext  8703  apneg  8704  mulext1  8705  mulext  8707  ltleap  8725  aprcl  8739  mulap0  8747  mulcanapd  8754  recapb  8764  rec11ap  8803  rec11rap  8804  divdivdivap  8806  ddcanap  8819  divadddivap  8820  prodgt0gt0  8944  prodgt0  8945  prodge0  8947  lemulge11  8959  lt2mul2div  8972  ltrec  8976  lerec  8977  lerec2  8982  ledivp1  8996  mulle0r  9037  nn0ge0div  9480  suprzclex  9491  qapne  9780  xrlelttr  9948  xrltletr  9949  xrre3  9964  xrrege0  9967  xaddge0  10020  xle2add  10021  xlt2add  10022  fzass4  10204  fzrev  10226  elfz1b  10232  eluzgtdifelfzo  10348  fzocatel  10350  zsupcllemstep  10394  zsupcllemex  10395  zssinfcl  10397  suprzubdc  10401  exbtwnzlemex  10414  rebtwn2z  10419  modqid  10516  modqcyc  10526  modqaddabs  10529  modqaddmod  10530  mulqaddmodid  10531  modqadd2mod  10541  modqltm1p1mod  10543  modqsubmod  10549  modqsubmodmod  10550  modaddmodup  10554  modqmulmod  10556  modqmulmodr  10557  modqaddmulmod  10558  modqsubdir  10560  frec2uzisod  10574  uzennn  10603  iseqovex  10625  seqvalcd  10628  seq1g  10630  seqf  10631  seqovcd  10634  seqclg  10639  seqm1g  10641  seq3shft2  10648  seqshft2g  10649  monoord  10652  iseqf1olemnab  10668  seqf1oglem1  10686  seqf1og  10688  seqhomog  10697  seqfeq4g  10698  seq3distr  10699  expnegzap  10740  ltexp2a  10758  le2sq2  10782  bernneq  10827  expnlbnd2  10832  nn0ltexp2  10876  nn0opth2  10891  faclbnd  10908  bcval5  10930  hashcl  10948  hashen  10951  fihashdom  10970  hashunlem  10971  hashun  10972  hashxp  10993  fimaxq  10994  zfz1isolem1  11007  zfz1iso  11008  seq3coll  11009  sswrd  11025  ccatw2s1p2  11120  wrdind  11198  cvg1nlemres  11371  cvg1n  11372  resqrexlemp1rp  11392  resqrexlemoverl  11407  resqrexlemex  11411  sqrtsq  11430  abslt  11474  absle  11475  abs3lem  11497  maxleastlt  11601  maxltsup  11604  fimaxre2  11613  negfi  11614  xrmaxleastlt  11642  xrmaxltsup  11644  xrmaxaddlem  11646  2clim  11687  climcn2  11695  addcn2  11696  mulcn2  11698  reccn2ap  11699  climge0  11711  climcau  11733  summodclem2  11768  summodc  11769  zsumdc  11770  fsumf1o  11776  fisumss  11778  fsum3cvg3  11782  fsumcl2lem  11784  fsumadd  11792  mptfzshft  11828  fsumrev  11829  fsummulc2  11834  fsumconst  11840  modfsummod  11844  fsumrelem  11857  binom  11870  cvgratnn  11917  mertenslemub  11920  prodmodclem2  11963  prodmodc  11964  zproddc  11965  fprodf1o  11974  fprodssdc  11976  fprodmul  11977  fprodcl2lem  11991  fprodrev  12005  fprodconst  12006  fprodap0  12007  fprodrec  12015  fprodap0f  12022  fprodle  12026  fprodmodd  12027  efcllem  12045  tanaddaplem  12124  moddvds  12185  dvdsflip  12237  oexpneg  12263  nn0o  12293  fldivndvdslt  12323  bitsfi  12343  bezoutlemnewy  12392  bezoutlemstep  12393  bezoutlemeu  12403  dfgcd3  12406  dfgcd2  12410  dvdsmulgcd  12421  bezoutr  12428  nninfctlemfo  12436  lcmgcdlem  12474  coprmdvds2  12490  qredeu  12494  rpdvds  12496  cncongr1  12500  prmind2  12517  isprm5lem  12538  isprm6  12544  oddpwdclemdc  12570  nonsq  12604  hashdvds  12618  crth  12621  eulerthlemh  12628  prmdiveq  12633  hashgcdlem  12635  hashgcdeq  12637  nnnn0modprm0  12653  pclemub  12685  pceu  12693  pcmul  12699  pcqmul  12701  pcgcd1  12726  pc2dvds  12728  difsqpwdvds  12736  pcmpt  12741  prmpwdvds  12753  1arith  12765  mul4sq  12792  4sqlemafi  12793  4sqlemffi  12794  4sqexercise2  12797  ennnfonelemg  12849  ennnfonelemex  12860  ennnfonelemrnh  12862  ennnfonelemf1  12864  ennnfonelemrn  12865  ennnfonelemdm  12866  ennnfonelemim  12870  ennnfone  12871  ctinf  12876  ctiunctlemfo  12885  nninfdclemcl  12894  nninfdclemf  12895  nninfdclemp1  12896  unbendc  12900  isstruct2r  12918  setscom  12947  ercpbl  13238  opifismgmdc  13278  grpinvalem  13292  igsumvalx  13296  gsumfzval  13298  gsumval2  13304  sgrppropd  13320  prdssgrpd  13322  mndpropd  13347  issubmnd  13349  submnd0  13351  prdsmndd  13355  mhmf1o  13377  subsubm  13390  0mhm  13393  resmhm  13394  mhmco  13397  mhmima  13398  mhmeql  13399  gsumfzz  13402  gsumwsubmcl  13403  gsumfzcl  13406  grprcan  13444  grpinvid1  13459  grpinvid2  13460  grplcan  13469  grplmulf1o  13481  grpnpncan0  13503  dfgrp3mlem  13505  grplactcnv  13509  pwssub  13520  mulgval  13533  mulgfng  13535  mulgnngsum  13538  mulg1  13540  mulgnnp1  13541  mulgneg  13551  mulgnndir  13562  mulgdirlem  13564  mulgnn0ass  13569  mulgass  13570  subgmulg  13599  issubg4m  13604  subsubg  13608  subgintm  13609  isnsg3  13618  eqgcpbl  13639  ghmeql  13678  ghmnsgima  13679  ghmnsgpreima  13680  ghmf1  13684  ghmf1o  13686  conjghm  13687  qusghm  13693  ablpncan3  13728  invghm  13740  eqgabl  13741  gsumfzreidx  13748  gsumfzsubmcl  13749  gsumfzmptfidmadd  13750  gsumfzmhm  13754  rngpropd  13792  imasrng  13793  qusrng  13795  srglmhm  13830  srgrmhm  13831  ringpropd  13875  ringlghm  13898  ringrghm  13899  imasring  13901  qusring2  13903  opprrngbg  13915  dvdsrvald  13930  dvdsrd  13931  dvdsrex  13935  dvdsrtr  13938  unitpropdg  13985  rhmopp  14013  isnzr2  14021  issubrng2  14047  subrngintm  14049  subsubrng  14051  subrgintm  14080  subsubrg  14082  rhmpropd  14091  aprap  14123  lmodprop2d  14185  rmodislmod  14188  lssvacl  14202  lssvsubcl  14203  lssvscl  14212  islss3  14216  lss1d  14220  rnglidlmcl  14317  2idlcpblrng  14360  crngridl  14367  expghmap  14444  mulgghm2  14445  mulgrhm  14446  znf1o  14488  znleval  14490  znidom  14494  znidomb  14495  znunit  14496  mplsubgfilemcl  14536  iuncld  14662  ssnei2  14704  topssnei  14709  restopnb  14728  cnfval  14741  cnpfval  14742  iscnp4  14765  cnptopco  14769  cncnpi  14775  cncnp  14777  cnconst2  14780  cnrest2  14783  cnptoprest  14786  cnptoprest2  14787  cnpdis  14789  lmss  14793  lmtopcnp  14797  neitx  14815  txcnp  14818  txrest  14823  txdis1cn  14825  txlm  14826  cnmpt21  14838  imasnopn  14846  xmetres2  14926  blvalps  14935  blval  14936  elbl2ps  14939  elbl2  14940  blhalf  14955  blssexps  14976  blssex  14977  ssblex  14978  blin2  14979  bdmetval  15047  xmetxp  15054  xmettx  15057  metcnpi3  15064  txmetcnp  15065  addcncntoplem  15108  fsumcncntop  15114  elcncf2  15121  mulc1cncf  15136  cncfco  15138  cncfmet  15139  cncfmptc  15143  mulcncf  15155  dedekindeulemub  15165  dedekindeulemloc  15166  dedekindeulemlu  15168  dedekindeu  15170  dedekindicclemub  15174  dedekindicclemloc  15175  dedekindicclemlu  15177  dedekindicclemicc  15179  dedekindicc  15180  ivthinclemlopn  15183  ivthinclemuopn  15185  dich0  15199  limcimo  15212  cnplimccntop  15217  limccnp2lem  15223  limccnp2cntop  15224  dvfvalap  15228  dveflem  15273  plycolemc  15305  plyco  15306  plyrecj  15310  reeff1olem  15318  reeff1oleme  15319  eflt  15322  sin0pilem2  15329  pilem3  15330  ioocosf1o  15401  cxplt  15463  cxple  15464  cxplt3  15467  apcxp2  15486  rprelogbmul  15502  rprelogbdiv  15504  logbgt0b  15513  logbgcd1irrap  15517  mpodvdsmulf1o  15537  fsumdvdsmul  15538  lgsdir2lem5  15584  lgsdi  15589  lgsne0  15590  gausslemma2dlem1f1o  15612  lgseisenlem2  15623  lgsquadlem1  15629  lgsquadlem2  15630  lgsquadlem3  15631  lgsquad2lem2  15634  lgsquad2  15635  2sqlem6  15672  2sqlem8  15675  2sqlem9  15676  2sqlem10  15677  nnti  16068  pwtrufal  16075  pwf1oexmid  16077  sssneq  16080  qdencn  16107  cvgcmp2n  16113  trilpolemlt1  16121  trirec0  16124  redc0  16137  reap0  16138  cndcap  16139  nconstwlpolemgt0  16144  neap0mkv  16149  supfz  16151  inffz  16152