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  4025  reg2exmidlema  4567  reg3exmidlemwe  4612  nnsucpred  4650  iotam  5247  fvmptt  5650  fcof1  5827  fliftfun  5840  isotr  5860  riotass2  5901  acexmidlemab  5913  ovmpodf  6051  fnmpoovd  6270  1stconst  6276  2ndconst  6277  cnvf1olem  6279  f1od2  6290  smoiso  6357  tfrcldm  6418  tfrcl  6419  nntr2  6558  swoer  6617  erinxp  6665  ecopovsymg  6690  th3qlem1  6693  f1imaen2g  6849  pw2f1odclem  6892  mapdom1g  6905  fict  6926  fidifsnen  6928  dif1enen  6938  fiunsnnn  6939  fisbth  6941  findcard2d  6949  findcard2sd  6950  diffifi  6952  ac6sfi  6956  fimax2gtri  6959  nnwetri  6974  unsnfi  6977  unsnfidcex  6978  unsnfidcel  6979  fisseneq  6990  ssfirab  6992  fidcenumlemrk  7015  fidcenumlemr  7016  sbthlemi6  7023  sbthlemi8  7025  isbth  7028  fiuni  7039  supmaxti  7065  infminti  7088  ordiso2  7096  eldju2ndl  7133  eldju2ndr  7134  omp1eomlem  7155  difinfsnlem  7160  difinfinf  7162  ctmlemr  7169  ctssdccl  7172  nninfninc  7184  fodjum  7207  fodju0  7208  omniwomnimkv  7228  exmidfodomrlemrALT  7265  acfun  7269  exmidaclem  7270  netap  7316  exmidmotap  7323  ccfunen  7326  cc1  7327  cc2lem  7328  dfplpq2  7416  dfmpq2  7417  mulpipqqs  7435  distrnqg  7449  enq0sym  7494  enq0tr  7496  distrnq0  7521  prarloclem3  7559  genplt2i  7572  addlocpr  7598  prmuloc  7628  distrlem1prl  7644  distrlem1pru  7645  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  ltaprg  7681  prplnqu  7682  addextpr  7683  recexprlemdisj  7692  recexprlemloc  7693  aptiprleml  7701  aptiprlemu  7702  ltmprr  7704  archpr  7705  cauappcvgprlemopl  7708  cauappcvgprlemopu  7710  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlem1  7721  cauappcvgprlemlim  7723  caucvgprlemnkj  7728  caucvgprlemopl  7731  caucvgprlemopu  7733  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemnjltk  7753  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemopu  7761  caucvgprprlemdisj  7764  caucvgprprlemloc  7765  caucvgprprlemaddq  7770  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemex  7784  suplocexprlemub  7785  recexgt0sr  7835  mulgt0sr  7840  prsrriota  7850  suplocsrlem  7870  addcnsr  7896  mulcnsr  7897  mulcnsrec  7905  axmulcom  7933  rereceu  7951  axarch  7953  axcaucvglemres  7961  axpre-suploclemres  7963  lelttr  8110  ltletr  8111  addcan  8201  addcan2  8202  addsub4  8264  ltadd2  8440  le2add  8465  lt2add  8466  lt2sub  8481  le2sub  8482  eqord1  8504  rereim  8607  apreap  8608  apreim  8624  mulreim  8625  apcotr  8628  apadd1  8629  addext  8631  apneg  8632  mulext1  8633  mulext  8635  ltleap  8653  aprcl  8667  mulap0  8675  mulcanapd  8682  recapb  8692  rec11ap  8731  rec11rap  8732  divdivdivap  8734  ddcanap  8747  divadddivap  8748  prodgt0gt0  8872  prodgt0  8873  prodge0  8875  lemulge11  8887  lt2mul2div  8900  ltrec  8904  lerec  8905  lerec2  8910  ledivp1  8924  mulle0r  8965  nn0ge0div  9407  suprzclex  9418  qapne  9707  xrlelttr  9875  xrltletr  9876  xrre3  9891  xrrege0  9894  xaddge0  9947  xle2add  9948  xlt2add  9949  fzass4  10131  fzrev  10153  elfz1b  10159  eluzgtdifelfzo  10267  fzocatel  10269  exbtwnzlemex  10321  rebtwn2z  10326  modqid  10423  modqcyc  10433  modqaddabs  10436  modqaddmod  10437  mulqaddmodid  10438  modqadd2mod  10448  modqltm1p1mod  10450  modqsubmod  10456  modqsubmodmod  10457  modaddmodup  10461  modqmulmod  10463  modqmulmodr  10464  modqaddmulmod  10465  modqsubdir  10467  frec2uzisod  10481  uzennn  10510  iseqovex  10532  seqvalcd  10535  seq1g  10537  seqf  10538  seqovcd  10541  seqclg  10546  seqm1g  10548  seq3shft2  10555  seqshft2g  10556  monoord  10559  iseqf1olemnab  10575  seqf1oglem1  10593  seqf1og  10595  seqhomog  10604  seqfeq4g  10605  seq3distr  10606  expnegzap  10647  ltexp2a  10665  le2sq2  10689  bernneq  10734  expnlbnd2  10739  nn0ltexp2  10783  nn0opth2  10798  faclbnd  10815  bcval5  10837  hashcl  10855  hashen  10858  fihashdom  10877  hashunlem  10878  hashun  10879  hashxp  10900  fimaxq  10901  zfz1isolem1  10914  zfz1iso  10915  seq3coll  10916  sswrd  10926  cvg1nlemres  11132  cvg1n  11133  resqrexlemp1rp  11153  resqrexlemoverl  11168  resqrexlemex  11172  sqrtsq  11191  abslt  11235  absle  11236  abs3lem  11258  maxleastlt  11362  maxltsup  11365  fimaxre2  11373  negfi  11374  xrmaxleastlt  11402  xrmaxltsup  11404  xrmaxaddlem  11406  2clim  11447  climcn2  11455  addcn2  11456  mulcn2  11458  reccn2ap  11459  climge0  11471  climcau  11493  summodclem2  11528  summodc  11529  zsumdc  11530  fsumf1o  11536  fisumss  11538  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  mptfzshft  11588  fsumrev  11589  fsummulc2  11594  fsumconst  11600  modfsummod  11604  fsumrelem  11617  binom  11630  cvgratnn  11677  mertenslemub  11680  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodf1o  11734  fprodssdc  11736  fprodmul  11737  fprodcl2lem  11751  fprodrev  11765  fprodconst  11766  fprodap0  11767  fprodrec  11775  fprodap0f  11782  fprodle  11786  fprodmodd  11787  efcllem  11805  tanaddaplem  11884  moddvds  11945  dvdsflip  11996  oexpneg  12021  nn0o  12051  fldivndvdslt  12079  zsupcllemstep  12085  zsupcllemex  12086  zssinfcl  12088  suprzubdc  12092  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemeu  12147  dfgcd3  12150  dfgcd2  12154  dvdsmulgcd  12165  bezoutr  12172  nninfctlemfo  12180  lcmgcdlem  12218  coprmdvds2  12234  qredeu  12238  rpdvds  12240  cncongr1  12244  prmind2  12261  isprm5lem  12282  isprm6  12288  oddpwdclemdc  12314  nonsq  12348  hashdvds  12362  crth  12365  eulerthlemh  12372  prmdiveq  12377  hashgcdlem  12379  hashgcdeq  12380  nnnn0modprm0  12396  pclemub  12428  pceu  12436  pcmul  12442  pcqmul  12444  pcgcd1  12469  pc2dvds  12471  difsqpwdvds  12479  pcmpt  12484  prmpwdvds  12496  1arith  12508  mul4sq  12535  4sqlemafi  12536  4sqlemffi  12537  4sqexercise2  12540  ennnfonelemg  12563  ennnfonelemex  12574  ennnfonelemrnh  12576  ennnfonelemf1  12578  ennnfonelemrn  12579  ennnfonelemdm  12580  ennnfonelemim  12584  ennnfone  12585  ctinf  12590  ctiunctlemfo  12599  nninfdclemcl  12608  nninfdclemf  12609  nninfdclemp1  12610  unbendc  12614  isstruct2r  12632  setscom  12661  ercpbl  12917  opifismgmdc  12957  grpinvalem  12971  igsumvalx  12975  gsumfzval  12977  gsumval2  12983  sgrppropd  12999  mndpropd  13024  issubmnd  13026  submnd0  13028  mhmf1o  13045  subsubm  13058  0mhm  13061  resmhm  13062  mhmco  13065  mhmima  13066  mhmeql  13067  gsumfzz  13070  gsumwsubmcl  13071  gsumfzcl  13074  grprcan  13112  grpinvid1  13127  grpinvid2  13128  grplcan  13137  grplmulf1o  13149  grpnpncan0  13171  dfgrp3mlem  13173  grplactcnv  13177  mulgval  13195  mulgfng  13197  mulgnngsum  13200  mulg1  13202  mulgnnp1  13203  mulgneg  13213  mulgnndir  13224  mulgdirlem  13226  mulgnn0ass  13231  mulgass  13232  subgmulg  13261  issubg4m  13266  subsubg  13270  subgintm  13271  isnsg3  13280  eqgcpbl  13301  ghmeql  13340  ghmnsgima  13341  ghmnsgpreima  13342  ghmf1  13346  ghmf1o  13348  conjghm  13349  qusghm  13355  ablpncan3  13390  invghm  13402  eqgabl  13403  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  rngpropd  13454  imasrng  13455  qusrng  13457  srglmhm  13492  srgrmhm  13493  ringpropd  13537  ringlghm  13560  ringrghm  13561  imasring  13563  qusring2  13565  opprrngbg  13577  dvdsrvald  13592  dvdsrd  13593  dvdsrex  13597  dvdsrtr  13600  unitpropdg  13647  rhmopp  13675  isnzr2  13683  issubrng2  13709  subrngintm  13711  subsubrng  13713  subrgintm  13742  subsubrg  13744  rhmpropd  13753  aprap  13785  lmodprop2d  13847  rmodislmod  13850  lssvacl  13864  lssvsubcl  13865  lssvscl  13874  islss3  13878  lss1d  13882  rnglidlmcl  13979  2idlcpblrng  14022  crngridl  14029  expghmap  14106  mulgghm2  14107  mulgrhm  14108  znf1o  14150  znleval  14152  znidom  14156  znidomb  14157  znunit  14158  iuncld  14294  ssnei2  14336  topssnei  14341  restopnb  14360  cnfval  14373  cnpfval  14374  iscnp4  14397  cnptopco  14401  cncnpi  14407  cncnp  14409  cnconst2  14412  cnrest2  14415  cnptoprest  14418  cnptoprest2  14419  cnpdis  14421  lmss  14425  lmtopcnp  14429  neitx  14447  txcnp  14450  txrest  14455  txdis1cn  14457  txlm  14458  cnmpt21  14470  imasnopn  14478  xmetres2  14558  blvalps  14567  blval  14568  elbl2ps  14571  elbl2  14572  blhalf  14587  blssexps  14608  blssex  14609  ssblex  14610  blin2  14611  bdmetval  14679  xmetxp  14686  xmettx  14689  metcnpi3  14696  txmetcnp  14697  addcncntoplem  14740  fsumcncntop  14746  elcncf2  14753  mulc1cncf  14768  cncfco  14770  cncfmet  14771  cncfmptc  14775  mulcncf  14787  dedekindeulemub  14797  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeu  14802  dedekindicclemub  14806  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicclemicc  14811  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemuopn  14817  dich0  14831  limcimo  14844  cnplimccntop  14849  limccnp2lem  14855  limccnp2cntop  14856  dvfvalap  14860  dveflem  14905  plycolemc  14936  plyco  14937  plyrecj  14941  reeff1olem  14947  reeff1oleme  14948  eflt  14951  sin0pilem2  14958  pilem3  14959  ioocosf1o  15030  cxplt  15091  cxple  15092  cxplt3  15095  apcxp2  15113  rprelogbmul  15128  rprelogbdiv  15130  logbgt0b  15139  logbgcd1irrap  15143  lgsdir2lem5  15189  lgsdi  15194  lgsne0  15195  gausslemma2dlem1f1o  15217  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem2  15239  lgsquad2  15240  2sqlem6  15277  2sqlem8  15280  2sqlem9  15281  2sqlem10  15282  nnti  15555  pwtrufal  15558  pwf1oexmid  15560  sssneq  15562  qdencn  15587  cvgcmp2n  15593  trilpolemlt1  15601  trirec0  15604  redc0  15617  reap0  15618  cndcap  15619  nconstwlpolemgt0  15624  neap0mkv  15629  supfz  15631  inffz  15632