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  1053  simp2rr  1057  simp3rr  1061  disjiun  3976  reg2exmidlema  4510  reg3exmidlemwe  4555  nnsucpred  4593  fvmptt  5576  fcof1  5750  fliftfun  5763  isotr  5783  riotass2  5823  acexmidlemab  5835  ovmpodf  5969  grprinvlem  6032  fnmpoovd  6179  1stconst  6185  2ndconst  6186  cnvf1olem  6188  f1od2  6199  smoiso  6266  tfrcldm  6327  tfrcl  6328  nntr2  6467  swoer  6525  erinxp  6571  ecopovsymg  6596  th3qlem1  6599  f1imaen2g  6755  mapdom1g  6809  fict  6830  fidifsnen  6832  dif1enen  6842  fiunsnnn  6843  fisbth  6845  findcard2d  6853  findcard2sd  6854  diffifi  6856  ac6sfi  6860  fimax2gtri  6863  nnwetri  6877  unsnfi  6880  unsnfidcex  6881  unsnfidcel  6882  fisseneq  6893  ssfirab  6895  fidcenumlemrk  6915  fidcenumlemr  6916  sbthlemi6  6923  sbthlemi8  6925  isbth  6928  fiuni  6939  supmaxti  6965  infminti  6988  ordiso2  6996  eldju2ndl  7033  eldju2ndr  7034  omp1eomlem  7055  difinfsnlem  7060  difinfinf  7062  ctmlemr  7069  ctssdccl  7072  fodjum  7106  fodju0  7107  omniwomnimkv  7127  exmidfodomrlemrALT  7155  acfun  7159  exmidaclem  7160  ccfunen  7201  cc1  7202  cc2lem  7203  dfplpq2  7291  dfmpq2  7292  mulpipqqs  7310  distrnqg  7324  enq0sym  7369  enq0tr  7371  distrnq0  7396  prarloclem3  7434  genplt2i  7447  addlocpr  7473  prmuloc  7503  distrlem1prl  7519  distrlem1pru  7520  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemfl  7546  ltexprlemrl  7547  ltexprlemfu  7548  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  ltaprg  7556  prplnqu  7557  addextpr  7558  recexprlemdisj  7567  recexprlemloc  7568  aptiprleml  7576  aptiprlemu  7577  ltmprr  7579  archpr  7580  cauappcvgprlemopl  7583  cauappcvgprlemopu  7585  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlem1  7596  cauappcvgprlemlim  7598  caucvgprlemnkj  7603  caucvgprlemopl  7606  caucvgprlemopu  7608  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprprlemnkltj  7626  caucvgprprlemnkeqj  7627  caucvgprprlemnjltk  7628  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemopu  7636  caucvgprprlemdisj  7639  caucvgprprlemloc  7640  caucvgprprlemaddq  7645  suplocexprlemrl  7654  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemex  7659  suplocexprlemub  7660  recexgt0sr  7710  mulgt0sr  7715  prsrriota  7725  suplocsrlem  7745  addcnsr  7771  mulcnsr  7772  mulcnsrec  7780  axmulcom  7808  rereceu  7826  axarch  7828  axcaucvglemres  7836  axpre-suploclemres  7838  lelttr  7983  ltletr  7984  addcan  8074  addcan2  8075  addsub4  8137  ltadd2  8313  le2add  8338  lt2add  8339  lt2sub  8354  le2sub  8355  eqord1  8377  rereim  8480  apreap  8481  apreim  8497  mulreim  8498  apcotr  8501  apadd1  8502  addext  8504  apneg  8505  mulext1  8506  mulext  8508  ltleap  8526  aprcl  8540  mulap0  8547  mulcanapd  8554  rec11ap  8602  rec11rap  8603  divdivdivap  8605  ddcanap  8618  divadddivap  8619  prodgt0gt0  8742  prodgt0  8743  prodge0  8745  lemulge11  8757  lt2mul2div  8770  ltrec  8774  lerec  8775  lerec2  8780  ledivp1  8794  mulle0r  8835  nn0ge0div  9274  suprzclex  9285  qapne  9573  xrlelttr  9738  xrltletr  9739  xrre3  9754  xrrege0  9757  xaddge0  9810  xle2add  9811  xlt2add  9812  fzass4  9993  fzrev  10015  elfz1b  10021  eluzgtdifelfzo  10128  fzocatel  10130  exbtwnzlemex  10181  rebtwn2z  10186  modqid  10280  modqcyc  10290  modqaddabs  10293  modqaddmod  10294  mulqaddmodid  10295  modqadd2mod  10305  modqltm1p1mod  10307  modqsubmod  10313  modqsubmodmod  10314  modaddmodup  10318  modqmulmod  10320  modqmulmodr  10321  modqaddmulmod  10322  modqsubdir  10324  frec2uzisod  10338  uzennn  10367  iseqovex  10387  seqvalcd  10390  seqf  10392  seqovcd  10394  seq3shft2  10404  monoord  10407  iseqf1olemnab  10419  seq3distr  10444  expnegzap  10485  ltexp2a  10503  le2sq2  10526  bernneq  10571  expnlbnd2  10576  nn0ltexp2  10619  nn0opth2  10633  faclbnd  10650  bcval5  10672  hashcl  10690  hashen  10693  fihashdom  10712  hashunlem  10713  hashun  10714  hashxp  10735  fimaxq  10736  zfz1isolem1  10749  zfz1iso  10750  seq3coll  10751  cvg1nlemres  10923  cvg1n  10924  resqrexlemp1rp  10944  resqrexlemoverl  10959  resqrexlemex  10963  sqrtsq  10982  abslt  11026  absle  11027  abs3lem  11049  maxleastlt  11153  maxltsup  11156  fimaxre2  11164  negfi  11165  xrmaxleastlt  11193  xrmaxltsup  11195  xrmaxaddlem  11197  2clim  11238  climcn2  11246  addcn2  11247  mulcn2  11249  reccn2ap  11250  climge0  11262  climcau  11284  summodclem2  11319  summodc  11320  zsumdc  11321  fsumf1o  11327  fisumss  11329  fsum3cvg3  11333  fsumcl2lem  11335  fsumadd  11343  mptfzshft  11379  fsumrev  11380  fsummulc2  11385  fsumconst  11391  modfsummod  11395  fsumrelem  11408  binom  11421  cvgratnn  11468  mertenslemub  11471  prodmodclem2  11514  prodmodc  11515  zproddc  11516  fprodf1o  11525  fprodssdc  11527  fprodmul  11528  fprodcl2lem  11542  fprodrev  11556  fprodconst  11557  fprodap0  11558  fprodrec  11566  fprodap0f  11573  fprodle  11577  fprodmodd  11578  efcllem  11596  tanaddaplem  11675  moddvds  11735  dvdsflip  11785  oexpneg  11810  nn0o  11840  fldivndvdslt  11868  zsupcllemstep  11874  zsupcllemex  11875  zssinfcl  11877  suprzubdc  11881  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemeu  11936  dfgcd3  11939  dfgcd2  11943  dvdsmulgcd  11954  bezoutr  11961  lcmgcdlem  12005  coprmdvds2  12021  qredeu  12025  rpdvds  12027  cncongr1  12031  prmind2  12048  isprm5lem  12069  isprm6  12075  oddpwdclemdc  12101  nonsq  12135  hashdvds  12149  crth  12152  eulerthlemh  12159  prmdiveq  12164  hashgcdlem  12166  hashgcdeq  12167  nnnn0modprm0  12183  pclemub  12215  pceu  12223  pcmul  12229  pcqmul  12231  pcgcd1  12255  pc2dvds  12257  difsqpwdvds  12265  pcmpt  12269  prmpwdvds  12281  1arith  12293  mul4sq  12320  ennnfonelemg  12332  ennnfonelemex  12343  ennnfonelemrnh  12345  ennnfonelemf1  12347  ennnfonelemrn  12348  ennnfonelemdm  12349  ennnfonelemim  12353  ennnfone  12354  ctinf  12359  ctiunctlemfo  12368  nninfdclemcl  12377  nninfdclemf  12378  nninfdclemp1  12379  unbendc  12383  isstruct2r  12401  setscom  12430  iuncld  12715  ssnei2  12757  topssnei  12762  restopnb  12781  cnfval  12794  cnpfval  12795  iscnp4  12818  cnptopco  12822  cncnpi  12828  cncnp  12830  cnconst2  12833  cnrest2  12836  cnptoprest  12839  cnptoprest2  12840  cnpdis  12842  lmss  12846  lmtopcnp  12850  neitx  12868  txcnp  12871  txrest  12876  txdis1cn  12878  txlm  12879  cnmpt21  12891  imasnopn  12899  xmetres2  12979  blvalps  12988  blval  12989  elbl2ps  12992  elbl2  12993  blhalf  13008  blssexps  13029  blssex  13030  ssblex  13031  blin2  13032  bdmetval  13100  xmetxp  13107  xmettx  13110  metcnpi3  13117  txmetcnp  13118  addcncntoplem  13151  fsumcncntop  13156  elcncf2  13161  mulc1cncf  13176  cncfco  13178  cncfmet  13179  cncfmptc  13182  mulcncf  13191  dedekindeulemub  13196  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeu  13201  dedekindicclemub  13205  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicclemicc  13210  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemuopn  13216  limcimo  13234  cnplimccntop  13239  limccnp2lem  13245  limccnp2cntop  13246  dvfvalap  13250  dveflem  13287  reeff1olem  13292  reeff1oleme  13293  eflt  13296  sin0pilem2  13303  pilem3  13304  ioocosf1o  13375  cxplt  13436  cxple  13437  cxplt3  13440  apcxp2  13458  rprelogbmul  13473  rprelogbdiv  13475  logbgt0b  13484  logbgcd1irrap  13488  lgsdir2lem5  13533  lgsdi  13538  lgsne0  13539  2sqlem6  13556  2sqlem8  13559  2sqlem9  13560  2sqlem10  13561  nnti  13834  pwtrufal  13837  pwf1oexmid  13839  sssneq  13842  qdencn  13866  cvgcmp2n  13872  trilpolemlt1  13880  trirec0  13883  redc0  13896  reap0  13897  nconstwlpolemgt0  13902  supfz  13907  inffz  13908