Theorem simprr 522

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 483	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1rr  1048  simp2rr  1052  simp3rr  1056  disjiun  3956  reg2exmidlema  4487  reg3exmidlemwe  4532  nnsucpred  4570  fvmptt  5552  fcof1  5724  fliftfun  5737  isotr  5757  riotass2  5796  acexmidlemab  5808  ovmpodf  5942  grprinvlem  6005  fnmpoovd  6152  1stconst  6158  2ndconst  6159  cnvf1olem  6161  f1od2  6172  smoiso  6239  tfrcldm  6300  tfrcl  6301  nntr2  6439  swoer  6497  erinxp  6543  ecopovsymg  6568  th3qlem1  6571  f1imaen2g  6727  mapdom1g  6781  fict  6802  fidifsnen  6804  dif1enen  6814  fiunsnnn  6815  fisbth  6817  findcard2d  6825  findcard2sd  6826  diffifi  6828  ac6sfi  6832  fimax2gtri  6835  nnwetri  6849  unsnfi  6852  unsnfidcex  6853  unsnfidcel  6854  fisseneq  6865  ssfirab  6867  fidcenumlemrk  6887  fidcenumlemr  6888  sbthlemi6  6895  sbthlemi8  6897  isbth  6900  fiuni  6911  supmaxti  6936  infminti  6959  ordiso2  6965  eldju2ndl  7002  eldju2ndr  7003  omp1eomlem  7024  difinfsnlem  7029  difinfinf  7031  ctmlemr  7038  ctssdccl  7041  fodjum  7068  fodju0  7069  omniwomnimkv  7089  exmidfodomrlemrALT  7117  acfun  7121  exmidaclem  7122  ccfunen  7163  cc1  7164  cc2lem  7165  dfplpq2  7253  dfmpq2  7254  mulpipqqs  7272  distrnqg  7286  enq0sym  7331  enq0tr  7333  distrnq0  7358  prarloclem3  7396  genplt2i  7409  addlocpr  7435  prmuloc  7465  distrlem1prl  7481  distrlem1pru  7482  ltexprlemopl  7500  ltexprlemopu  7502  ltexprlemfl  7508  ltexprlemrl  7509  ltexprlemfu  7510  ltexprlemru  7511  addcanprleml  7513  addcanprlemu  7514  ltaprg  7518  prplnqu  7519  addextpr  7520  recexprlemdisj  7529  recexprlemloc  7530  aptiprleml  7538  aptiprlemu  7539  ltmprr  7541  archpr  7542  cauappcvgprlemopl  7545  cauappcvgprlemopu  7547  cauappcvgprlemdisj  7550  cauappcvgprlemloc  7551  cauappcvgprlem1  7558  cauappcvgprlemlim  7560  caucvgprlemnkj  7565  caucvgprlemopl  7568  caucvgprlemopu  7570  caucvgprlemdisj  7573  caucvgprlemloc  7574  caucvgprprlemnkltj  7588  caucvgprprlemnkeqj  7589  caucvgprprlemnjltk  7590  caucvgprprlemml  7593  caucvgprprlemmu  7594  caucvgprprlemopl  7596  caucvgprprlemopu  7598  caucvgprprlemdisj  7601  caucvgprprlemloc  7602  caucvgprprlemaddq  7607  suplocexprlemrl  7616  suplocexprlemmu  7617  suplocexprlemru  7618  suplocexprlemdisj  7619  suplocexprlemloc  7620  suplocexprlemex  7621  suplocexprlemub  7622  recexgt0sr  7672  mulgt0sr  7677  prsrriota  7687  suplocsrlem  7707  addcnsr  7733  mulcnsr  7734  mulcnsrec  7742  axmulcom  7770  rereceu  7788  axarch  7790  axcaucvglemres  7798  axpre-suploclemres  7800  lelttr  7944  ltletr  7945  addcan  8034  addcan2  8035  addsub4  8097  ltadd2  8273  le2add  8298  lt2add  8299  lt2sub  8314  le2sub  8315  eqord1  8337  rereim  8440  apreap  8441  apreim  8457  mulreim  8458  apcotr  8461  apadd1  8462  addext  8464  apneg  8465  mulext1  8466  mulext  8468  ltleap  8486  aprcl  8500  mulap0  8507  mulcanapd  8514  rec11ap  8562  rec11rap  8563  divdivdivap  8565  ddcanap  8578  divadddivap  8579  prodgt0gt0  8701  prodgt0  8702  prodge0  8704  lemulge11  8716  lt2mul2div  8729  ltrec  8733  lerec  8734  lerec2  8739  ledivp1  8753  mulle0r  8794  nn0ge0div  9230  suprzclex  9241  qapne  9526  xrlelttr  9688  xrltletr  9689  xrre3  9704  xrrege0  9707  xaddge0  9760  xle2add  9761  xlt2add  9762  fzass4  9942  fzrev  9964  elfz1b  9970  eluzgtdifelfzo  10074  fzocatel  10076  exbtwnzlemex  10127  rebtwn2z  10132  modqid  10226  modqcyc  10236  modqaddabs  10239  modqaddmod  10240  mulqaddmodid  10241  modqadd2mod  10251  modqltm1p1mod  10253  modqsubmod  10259  modqsubmodmod  10260  modaddmodup  10264  modqmulmod  10266  modqmulmodr  10267  modqaddmulmod  10268  modqsubdir  10270  frec2uzisod  10284  uzennn  10313  iseqovex  10333  seqvalcd  10336  seqf  10338  seqovcd  10340  seq3shft2  10350  monoord  10353  iseqf1olemnab  10365  seq3distr  10390  expnegzap  10431  ltexp2a  10449  le2sq2  10472  bernneq  10516  expnlbnd2  10521  nn0opth2  10575  faclbnd  10592  bcval5  10614  hashcl  10632  hashen  10635  fihashdom  10654  hashunlem  10655  hashun  10656  hashxp  10677  fimaxq  10678  zfz1isolem1  10688  zfz1iso  10689  seq3coll  10690  cvg1nlemres  10862  cvg1n  10863  resqrexlemp1rp  10883  resqrexlemoverl  10898  resqrexlemex  10902  sqrtsq  10921  abslt  10965  absle  10966  abs3lem  10988  maxleastlt  11092  maxltsup  11095  fimaxre2  11103  negfi  11104  xrmaxleastlt  11130  xrmaxltsup  11132  xrmaxaddlem  11134  2clim  11175  climcn2  11183  addcn2  11184  mulcn2  11186  reccn2ap  11187  climge0  11199  climcau  11221  summodclem2  11256  summodc  11257  zsumdc  11258  fsumf1o  11264  fisumss  11266  fsum3cvg3  11270  fsumcl2lem  11272  fsumadd  11280  mptfzshft  11316  fsumrev  11317  fsummulc2  11322  fsumconst  11328  modfsummod  11332  fsumrelem  11345  binom  11358  cvgratnn  11405  mertenslemub  11408  prodmodclem2  11451  prodmodc  11452  zproddc  11453  fprodf1o  11462  fprodssdc  11464  fprodmul  11465  fprodcl2lem  11479  fprodrev  11493  fprodconst  11494  fprodap0  11495  fprodrec  11503  fprodap0f  11510  fprodle  11514  fprodmodd  11515  efcllem  11533  tanaddaplem  11612  moddvds  11669  dvdsflip  11716  oexpneg  11741  nn0o  11771  fldivndvdslt  11799  zsupcllemstep  11805  zsupcllemex  11806  zssinfcl  11808  bezoutlemnewy  11851  bezoutlemstep  11852  bezoutlemeu  11862  dfgcd3  11865  dfgcd2  11869  dvdsmulgcd  11880  bezoutr  11887  lcmgcdlem  11925  coprmdvds2  11941  qredeu  11945  rpdvds  11947  cncongr1  11951  prmind2  11968  isprm6  11992  oddpwdclemdc  12018  nonsq  12052  hashdvds  12064  crth  12067  hashgcdlem  12070  hashgcdeq  12071  ennnfonelemg  12083  ennnfonelemex  12094  ennnfonelemrnh  12096  ennnfonelemf1  12098  ennnfonelemrn  12099  ennnfonelemdm  12100  ennnfonelemim  12104  ennnfone  12105  ctinf  12110  ctiunctlemfo  12119  isstruct2r  12140  setscom  12169  iuncld  12454  ssnei2  12496  topssnei  12501  restopnb  12520  cnfval  12533  cnpfval  12534  iscnp4  12557  cnptopco  12561  cncnpi  12567  cncnp  12569  cnconst2  12572  cnrest2  12575  cnptoprest  12578  cnptoprest2  12579  cnpdis  12581  lmss  12585  lmtopcnp  12589  neitx  12607  txcnp  12610  txrest  12615  txdis1cn  12617  txlm  12618  cnmpt21  12630  imasnopn  12638  xmetres2  12718  blvalps  12727  blval  12728  elbl2ps  12731  elbl2  12732  blhalf  12747  blssexps  12768  blssex  12769  ssblex  12770  blin2  12771  bdmetval  12839  xmetxp  12846  xmettx  12849  metcnpi3  12856  txmetcnp  12857  addcncntoplem  12890  fsumcncntop  12895  elcncf2  12900  mulc1cncf  12915  cncfco  12917  cncfmet  12918  cncfmptc  12921  mulcncf  12930  dedekindeulemub  12935  dedekindeulemloc  12936  dedekindeulemlu  12938  dedekindeu  12940  dedekindicclemub  12944  dedekindicclemloc  12945  dedekindicclemlu  12947  dedekindicclemicc  12949  dedekindicc  12950  ivthinclemlopn  12953  ivthinclemuopn  12955  limcimo  12973  cnplimccntop  12978  limccnp2lem  12984  limccnp2cntop  12985  dvfvalap  12989  dveflem  13026  reeff1olem  13031  reeff1oleme  13032  eflt  13035  sin0pilem2  13042  pilem3  13043  ioocosf1o  13114  cxplt  13175  cxple  13176  cxplt3  13179  apcxp2  13197  rprelogbmul  13211  rprelogbdiv  13213  logbgt0b  13222  logbgcd1irrap  13226  nnti  13505  pwtrufal  13508  pwf1oexmid  13510  sssneq  13513  qdencn  13539  cvgcmp2n  13545  trilpolemlt1  13553  trirec0  13556  redc0  13569  reap0  13570  nconstwlpolemgt0  13575  supfz  13580  inffz  13581