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  4028  reg2exmidlema  4570  reg3exmidlemwe  4615  nnsucpred  4653  iotam  5250  fvmptt  5653  fcof1  5830  fliftfun  5843  isotr  5863  riotass2  5904  acexmidlemab  5916  ovmpodf  6054  fnmpoovd  6273  1stconst  6279  2ndconst  6280  cnvf1olem  6282  f1od2  6293  smoiso  6360  tfrcldm  6421  tfrcl  6422  nntr2  6561  swoer  6620  erinxp  6668  ecopovsymg  6693  th3qlem1  6696  f1imaen2g  6852  pw2f1odclem  6895  mapdom1g  6908  fict  6929  fidifsnen  6931  dif1enen  6941  fiunsnnn  6942  fisbth  6944  findcard2d  6952  findcard2sd  6953  diffifi  6955  ac6sfi  6959  fimax2gtri  6962  nnwetri  6977  unsnfi  6980  unsnfidcex  6981  unsnfidcel  6982  fisseneq  6995  ssfirab  6997  fidcenumlemrk  7020  fidcenumlemr  7021  sbthlemi6  7028  sbthlemi8  7030  isbth  7033  fiuni  7044  supmaxti  7070  infminti  7093  ordiso2  7101  eldju2ndl  7138  eldju2ndr  7139  omp1eomlem  7160  difinfsnlem  7165  difinfinf  7167  ctmlemr  7174  ctssdccl  7177  nninfninc  7189  fodjum  7212  fodju0  7213  omniwomnimkv  7233  exmidfodomrlemrALT  7270  acfun  7274  exmidaclem  7275  netap  7321  exmidmotap  7328  ccfunen  7331  cc1  7332  cc2lem  7333  dfplpq2  7421  dfmpq2  7422  mulpipqqs  7440  distrnqg  7454  enq0sym  7499  enq0tr  7501  distrnq0  7526  prarloclem3  7564  genplt2i  7577  addlocpr  7603  prmuloc  7633  distrlem1prl  7649  distrlem1pru  7650  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  ltaprg  7686  prplnqu  7687  addextpr  7688  recexprlemdisj  7697  recexprlemloc  7698  aptiprleml  7706  aptiprlemu  7707  ltmprr  7709  archpr  7710  cauappcvgprlemopl  7713  cauappcvgprlemopu  7715  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlem1  7726  cauappcvgprlemlim  7728  caucvgprlemnkj  7733  caucvgprlemopl  7736  caucvgprlemopu  7738  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemnjltk  7758  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemopu  7766  caucvgprprlemdisj  7769  caucvgprprlemloc  7770  caucvgprprlemaddq  7775  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemex  7789  suplocexprlemub  7790  recexgt0sr  7840  mulgt0sr  7845  prsrriota  7855  suplocsrlem  7875  addcnsr  7901  mulcnsr  7902  mulcnsrec  7910  axmulcom  7938  rereceu  7956  axarch  7958  axcaucvglemres  7966  axpre-suploclemres  7968  lelttr  8115  ltletr  8116  addcan  8206  addcan2  8207  addsub4  8269  ltadd2  8446  le2add  8471  lt2add  8472  lt2sub  8487  le2sub  8488  eqord1  8510  rereim  8613  apreap  8614  apreim  8630  mulreim  8631  apcotr  8634  apadd1  8635  addext  8637  apneg  8638  mulext1  8639  mulext  8641  ltleap  8659  aprcl  8673  mulap0  8681  mulcanapd  8688  recapb  8698  rec11ap  8737  rec11rap  8738  divdivdivap  8740  ddcanap  8753  divadddivap  8754  prodgt0gt0  8878  prodgt0  8879  prodge0  8881  lemulge11  8893  lt2mul2div  8906  ltrec  8910  lerec  8911  lerec2  8916  ledivp1  8930  mulle0r  8971  nn0ge0div  9413  suprzclex  9424  qapne  9713  xrlelttr  9881  xrltletr  9882  xrre3  9897  xrrege0  9900  xaddge0  9953  xle2add  9954  xlt2add  9955  fzass4  10137  fzrev  10159  elfz1b  10165  eluzgtdifelfzo  10273  fzocatel  10275  zsupcllemstep  10319  zsupcllemex  10320  zssinfcl  10322  suprzubdc  10326  exbtwnzlemex  10339  rebtwn2z  10344  modqid  10441  modqcyc  10451  modqaddabs  10454  modqaddmod  10455  mulqaddmodid  10456  modqadd2mod  10466  modqltm1p1mod  10468  modqsubmod  10474  modqsubmodmod  10475  modaddmodup  10479  modqmulmod  10481  modqmulmodr  10482  modqaddmulmod  10483  modqsubdir  10485  frec2uzisod  10499  uzennn  10528  iseqovex  10550  seqvalcd  10553  seq1g  10555  seqf  10556  seqovcd  10559  seqclg  10564  seqm1g  10566  seq3shft2  10573  seqshft2g  10574  monoord  10577  iseqf1olemnab  10593  seqf1oglem1  10611  seqf1og  10613  seqhomog  10622  seqfeq4g  10623  seq3distr  10624  expnegzap  10665  ltexp2a  10683  le2sq2  10707  bernneq  10752  expnlbnd2  10757  nn0ltexp2  10801  nn0opth2  10816  faclbnd  10833  bcval5  10855  hashcl  10873  hashen  10876  fihashdom  10895  hashunlem  10896  hashun  10897  hashxp  10918  fimaxq  10919  zfz1isolem1  10932  zfz1iso  10933  seq3coll  10934  sswrd  10944  cvg1nlemres  11150  cvg1n  11151  resqrexlemp1rp  11171  resqrexlemoverl  11186  resqrexlemex  11190  sqrtsq  11209  abslt  11253  absle  11254  abs3lem  11276  maxleastlt  11380  maxltsup  11383  fimaxre2  11392  negfi  11393  xrmaxleastlt  11421  xrmaxltsup  11423  xrmaxaddlem  11425  2clim  11466  climcn2  11474  addcn2  11475  mulcn2  11477  reccn2ap  11478  climge0  11490  climcau  11512  summodclem2  11547  summodc  11548  zsumdc  11549  fsumf1o  11555  fisumss  11557  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  mptfzshft  11607  fsumrev  11608  fsummulc2  11613  fsumconst  11619  modfsummod  11623  fsumrelem  11636  binom  11649  cvgratnn  11696  mertenslemub  11699  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodf1o  11753  fprodssdc  11755  fprodmul  11756  fprodcl2lem  11770  fprodrev  11784  fprodconst  11785  fprodap0  11786  fprodrec  11794  fprodap0f  11801  fprodle  11805  fprodmodd  11806  efcllem  11824  tanaddaplem  11903  moddvds  11964  dvdsflip  12016  oexpneg  12042  nn0o  12072  fldivndvdslt  12102  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemeu  12174  dfgcd3  12177  dfgcd2  12181  dvdsmulgcd  12192  bezoutr  12199  nninfctlemfo  12207  lcmgcdlem  12245  coprmdvds2  12261  qredeu  12265  rpdvds  12267  cncongr1  12271  prmind2  12288  isprm5lem  12309  isprm6  12315  oddpwdclemdc  12341  nonsq  12375  hashdvds  12389  crth  12392  eulerthlemh  12399  prmdiveq  12404  hashgcdlem  12406  hashgcdeq  12408  nnnn0modprm0  12424  pclemub  12456  pceu  12464  pcmul  12470  pcqmul  12472  pcgcd1  12497  pc2dvds  12499  difsqpwdvds  12507  pcmpt  12512  prmpwdvds  12524  1arith  12536  mul4sq  12563  4sqlemafi  12564  4sqlemffi  12565  4sqexercise2  12568  ennnfonelemg  12620  ennnfonelemex  12631  ennnfonelemrnh  12633  ennnfonelemf1  12635  ennnfonelemrn  12636  ennnfonelemdm  12637  ennnfonelemim  12641  ennnfone  12642  ctinf  12647  ctiunctlemfo  12656  nninfdclemcl  12665  nninfdclemf  12666  nninfdclemp1  12667  unbendc  12671  isstruct2r  12689  setscom  12718  ercpbl  12974  opifismgmdc  13014  grpinvalem  13028  igsumvalx  13032  gsumfzval  13034  gsumval2  13040  sgrppropd  13056  mndpropd  13081  issubmnd  13083  submnd0  13085  mhmf1o  13102  subsubm  13115  0mhm  13118  resmhm  13119  mhmco  13122  mhmima  13123  mhmeql  13124  gsumfzz  13127  gsumwsubmcl  13128  gsumfzcl  13131  grprcan  13169  grpinvid1  13184  grpinvid2  13185  grplcan  13194  grplmulf1o  13206  grpnpncan0  13228  dfgrp3mlem  13230  grplactcnv  13234  mulgval  13252  mulgfng  13254  mulgnngsum  13257  mulg1  13259  mulgnnp1  13260  mulgneg  13270  mulgnndir  13281  mulgdirlem  13283  mulgnn0ass  13288  mulgass  13289  subgmulg  13318  issubg4m  13323  subsubg  13327  subgintm  13328  isnsg3  13337  eqgcpbl  13358  ghmeql  13397  ghmnsgima  13398  ghmnsgpreima  13399  ghmf1  13403  ghmf1o  13405  conjghm  13406  qusghm  13412  ablpncan3  13447  invghm  13459  eqgabl  13460  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  rngpropd  13511  imasrng  13512  qusrng  13514  srglmhm  13549  srgrmhm  13550  ringpropd  13594  ringlghm  13617  ringrghm  13618  imasring  13620  qusring2  13622  opprrngbg  13634  dvdsrvald  13649  dvdsrd  13650  dvdsrex  13654  dvdsrtr  13657  unitpropdg  13704  rhmopp  13732  isnzr2  13740  issubrng2  13766  subrngintm  13768  subsubrng  13770  subrgintm  13799  subsubrg  13801  rhmpropd  13810  aprap  13842  lmodprop2d  13904  rmodislmod  13907  lssvacl  13921  lssvsubcl  13922  lssvscl  13931  islss3  13935  lss1d  13939  rnglidlmcl  14036  2idlcpblrng  14079  crngridl  14086  expghmap  14163  mulgghm2  14164  mulgrhm  14165  znf1o  14207  znleval  14209  znidom  14213  znidomb  14214  znunit  14215  iuncld  14351  ssnei2  14393  topssnei  14398  restopnb  14417  cnfval  14430  cnpfval  14431  iscnp4  14454  cnptopco  14458  cncnpi  14464  cncnp  14466  cnconst2  14469  cnrest2  14472  cnptoprest  14475  cnptoprest2  14476  cnpdis  14478  lmss  14482  lmtopcnp  14486  neitx  14504  txcnp  14507  txrest  14512  txdis1cn  14514  txlm  14515  cnmpt21  14527  imasnopn  14535  xmetres2  14615  blvalps  14624  blval  14625  elbl2ps  14628  elbl2  14629  blhalf  14644  blssexps  14665  blssex  14666  ssblex  14667  blin2  14668  bdmetval  14736  xmetxp  14743  xmettx  14746  metcnpi3  14753  txmetcnp  14754  addcncntoplem  14797  fsumcncntop  14803  elcncf2  14810  mulc1cncf  14825  cncfco  14827  cncfmet  14828  cncfmptc  14832  mulcncf  14844  dedekindeulemub  14854  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeu  14859  dedekindicclemub  14863  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicclemicc  14868  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemuopn  14874  dich0  14888  limcimo  14901  cnplimccntop  14906  limccnp2lem  14912  limccnp2cntop  14913  dvfvalap  14917  dveflem  14962  plycolemc  14994  plyco  14995  plyrecj  14999  reeff1olem  15007  reeff1oleme  15008  eflt  15011  sin0pilem2  15018  pilem3  15019  ioocosf1o  15090  cxplt  15152  cxple  15153  cxplt3  15156  apcxp2  15175  rprelogbmul  15191  rprelogbdiv  15193  logbgt0b  15202  logbgcd1irrap  15206  mpodvdsmulf1o  15226  fsumdvdsmul  15227  lgsdir2lem5  15273  lgsdi  15278  lgsne0  15279  gausslemma2dlem1f1o  15301  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem2  15323  lgsquad2  15324  2sqlem6  15361  2sqlem8  15364  2sqlem9  15365  2sqlem10  15366  nnti  15639  pwtrufal  15642  pwf1oexmid  15644  sssneq  15646  qdencn  15671  cvgcmp2n  15677  trilpolemlt1  15685  trirec0  15688  redc0  15701  reap0  15702  cndcap  15703  nconstwlpolemgt0  15708  neap0mkv  15713  supfz  15715  inffz  15716