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:  dfifp2dc  987  simp1rr  1087  simp2rr  1091  simp3rr  1095  elpr2elpr  3854  invdisjrab  4077  disjiun  4078  reg2exmidlema  4626  reg3exmidlemwe  4671  nnsucpred  4709  iotam  5310  fvmptt  5728  fcof1  5913  fliftfun  5926  isotr  5946  riotass2  5989  acexmidlemab  6001  ovmpodf  6142  fnmpoovd  6367  1stconst  6373  2ndconst  6374  cnvf1olem  6376  f1od2  6387  smoiso  6454  tfrcldm  6515  tfrcl  6516  nntr2  6657  swoer  6716  erinxp  6764  ecopovsymg  6789  th3qlem1  6792  f1imaen2g  6953  pw2f1odclem  7003  mapdom1g  7016  fict  7038  fidifsnen  7040  dif1enen  7050  fiunsnnn  7051  fisbth  7053  findcard2d  7061  findcard2sd  7062  diffifi  7064  ac6sfi  7068  fimax2gtri  7072  nnwetri  7089  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  fisseneq  7107  ssfirab  7109  fidcenumlemrk  7132  fidcenumlemr  7133  sbthlemi6  7140  sbthlemi8  7142  isbth  7145  fiuni  7156  supmaxti  7182  infminti  7205  ordiso2  7213  eldju2ndl  7250  eldju2ndr  7251  omp1eomlem  7272  difinfsnlem  7277  difinfinf  7279  ctmlemr  7286  ctssdccl  7289  nninfninc  7301  fodjum  7324  fodju0  7325  omniwomnimkv  7345  exmidfodomrlemrALT  7392  acfun  7400  exmidaclem  7401  netap  7451  exmidmotap  7458  ccfunen  7461  cc1  7462  cc2lem  7463  dfplpq2  7552  dfmpq2  7553  mulpipqqs  7571  distrnqg  7585  enq0sym  7630  enq0tr  7632  distrnq0  7657  prarloclem3  7695  genplt2i  7708  addlocpr  7734  prmuloc  7764  distrlem1prl  7780  distrlem1pru  7781  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  ltaprg  7817  prplnqu  7818  addextpr  7819  recexprlemdisj  7828  recexprlemloc  7829  aptiprleml  7837  aptiprlemu  7838  ltmprr  7840  archpr  7841  cauappcvgprlemopl  7844  cauappcvgprlemopu  7846  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  caucvgprlemnkj  7864  caucvgprlemopl  7867  caucvgprlemopu  7869  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnjltk  7889  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemdisj  7900  caucvgprprlemloc  7901  caucvgprprlemaddq  7906  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  recexgt0sr  7971  mulgt0sr  7976  prsrriota  7986  suplocsrlem  8006  addcnsr  8032  mulcnsr  8033  mulcnsrec  8041  axmulcom  8069  rereceu  8087  axarch  8089  axcaucvglemres  8097  axpre-suploclemres  8099  lelttr  8246  ltletr  8247  addcan  8337  addcan2  8338  addsub4  8400  ltadd2  8577  le2add  8602  lt2add  8603  lt2sub  8618  le2sub  8619  eqord1  8641  rereim  8744  apreap  8745  apreim  8761  mulreim  8762  apcotr  8765  apadd1  8766  addext  8768  apneg  8769  mulext1  8770  mulext  8772  ltleap  8790  aprcl  8804  mulap0  8812  mulcanapd  8819  recapb  8829  rec11ap  8868  rec11rap  8869  divdivdivap  8871  ddcanap  8884  divadddivap  8885  prodgt0gt0  9009  prodgt0  9010  prodge0  9012  lemulge11  9024  lt2mul2div  9037  ltrec  9041  lerec  9042  lerec2  9047  ledivp1  9061  mulle0r  9102  nn0ge0div  9545  suprzclex  9556  qapne  9846  xrlelttr  10014  xrltletr  10015  xrre3  10030  xrrege0  10033  xaddge0  10086  xle2add  10087  xlt2add  10088  fzass4  10270  fzrev  10292  elfz1b  10298  eluzgtdifelfzo  10415  fzocatel  10417  zsupcllemstep  10461  zsupcllemex  10462  zssinfcl  10464  suprzubdc  10468  exbtwnzlemex  10481  rebtwn2z  10486  modqid  10583  modqcyc  10593  modqaddabs  10596  modqaddmod  10597  mulqaddmodid  10598  modqadd2mod  10608  modqltm1p1mod  10610  modqsubmod  10616  modqsubmodmod  10617  modaddmodup  10621  modqmulmod  10623  modqmulmodr  10624  modqaddmulmod  10625  modqsubdir  10627  frec2uzisod  10641  uzennn  10670  iseqovex  10692  seqvalcd  10695  seq1g  10697  seqf  10698  seqovcd  10701  seqclg  10706  seqm1g  10708  seq3shft2  10715  seqshft2g  10716  monoord  10719  iseqf1olemnab  10735  seqf1oglem1  10753  seqf1og  10755  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  expnegzap  10807  ltexp2a  10825  le2sq2  10849  bernneq  10894  expnlbnd2  10899  nn0ltexp2  10943  nn0opth2  10958  faclbnd  10975  bcval5  10997  hashcl  11015  hashen  11018  fihashdom  11037  hashunlem  11038  hashun  11039  hashxp  11061  fimaxq  11062  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  sswrd  11093  ccatw2s1p2  11191  wrdind  11269  pfxccatin12lem1  11275  pfxccatin12lem3  11279  reuccatpfxs1lem  11293  cvg1nlemres  11511  cvg1n  11512  resqrexlemp1rp  11532  resqrexlemoverl  11547  resqrexlemex  11551  sqrtsq  11570  abslt  11614  absle  11615  abs3lem  11637  maxleastlt  11741  maxltsup  11744  fimaxre2  11753  negfi  11754  xrmaxleastlt  11782  xrmaxltsup  11784  xrmaxaddlem  11786  2clim  11827  climcn2  11835  addcn2  11836  mulcn2  11838  reccn2ap  11839  climge0  11851  climcau  11873  summodclem2  11908  summodc  11909  zsumdc  11910  fsumf1o  11916  fisumss  11918  fsum3cvg3  11922  fsumcl2lem  11924  fsumadd  11932  mptfzshft  11968  fsumrev  11969  fsummulc2  11974  fsumconst  11980  modfsummod  11984  fsumrelem  11997  binom  12010  cvgratnn  12057  mertenslemub  12060  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodf1o  12114  fprodssdc  12116  fprodmul  12117  fprodcl2lem  12131  fprodrev  12145  fprodconst  12146  fprodap0  12147  fprodrec  12155  fprodap0f  12162  fprodle  12166  fprodmodd  12167  efcllem  12185  tanaddaplem  12264  moddvds  12325  dvdsflip  12377  oexpneg  12403  nn0o  12433  fldivndvdslt  12463  bitsfi  12483  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemeu  12543  dfgcd3  12546  dfgcd2  12550  dvdsmulgcd  12561  bezoutr  12568  nninfctlemfo  12576  lcmgcdlem  12614  coprmdvds2  12630  qredeu  12634  rpdvds  12636  cncongr1  12640  prmind2  12657  isprm5lem  12678  isprm6  12684  oddpwdclemdc  12710  nonsq  12744  hashdvds  12758  crth  12761  eulerthlemh  12768  prmdiveq  12773  hashgcdlem  12775  hashgcdeq  12777  nnnn0modprm0  12793  pclemub  12825  pceu  12833  pcmul  12839  pcqmul  12841  pcgcd1  12866  pc2dvds  12868  difsqpwdvds  12876  pcmpt  12881  prmpwdvds  12893  1arith  12905  mul4sq  12932  4sqlemafi  12933  4sqlemffi  12934  4sqexercise2  12937  ennnfonelemg  12989  ennnfonelemex  13000  ennnfonelemrnh  13002  ennnfonelemf1  13004  ennnfonelemrn  13005  ennnfonelemdm  13006  ennnfonelemim  13010  ennnfone  13011  ctinf  13016  ctiunctlemfo  13025  nninfdclemcl  13034  nninfdclemf  13035  nninfdclemp1  13036  unbendc  13040  isstruct2r  13058  setscom  13087  ercpbl  13379  opifismgmdc  13419  grpinvalem  13433  igsumvalx  13437  gsumfzval  13439  gsumval2  13445  sgrppropd  13461  prdssgrpd  13463  mndpropd  13488  issubmnd  13490  submnd0  13492  prdsmndd  13496  mhmf1o  13518  subsubm  13531  0mhm  13534  resmhm  13535  mhmco  13538  mhmima  13539  mhmeql  13540  gsumfzz  13543  gsumwsubmcl  13544  gsumfzcl  13547  grprcan  13585  grpinvid1  13600  grpinvid2  13601  grplcan  13610  grplmulf1o  13622  grpnpncan0  13644  dfgrp3mlem  13646  grplactcnv  13650  pwssub  13661  mulgval  13674  mulgfng  13676  mulgnngsum  13679  mulg1  13681  mulgnnp1  13682  mulgneg  13692  mulgnndir  13703  mulgdirlem  13705  mulgnn0ass  13710  mulgass  13711  subgmulg  13740  issubg4m  13745  subsubg  13749  subgintm  13750  isnsg3  13759  eqgcpbl  13780  ghmeql  13819  ghmnsgima  13820  ghmnsgpreima  13821  ghmf1  13825  ghmf1o  13827  conjghm  13828  qusghm  13834  ablpncan3  13869  invghm  13881  eqgabl  13882  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  rngpropd  13933  imasrng  13934  qusrng  13936  srglmhm  13971  srgrmhm  13972  ringpropd  14016  ringlghm  14039  ringrghm  14040  imasring  14042  qusring2  14044  opprrngbg  14056  dvdsrvald  14072  dvdsrd  14073  dvdsrex  14077  dvdsrtr  14080  unitpropdg  14127  rhmopp  14155  isnzr2  14163  issubrng2  14189  subrngintm  14191  subsubrng  14193  subrgintm  14222  subsubrg  14224  rhmpropd  14233  aprap  14265  lmodprop2d  14327  rmodislmod  14330  lssvacl  14344  lssvsubcl  14345  lssvscl  14354  islss3  14358  lss1d  14362  rnglidlmcl  14459  2idlcpblrng  14502  crngridl  14509  expghmap  14586  mulgghm2  14587  mulgrhm  14588  znf1o  14630  znleval  14632  znidom  14636  znidomb  14637  znunit  14638  mplsubgfilemcl  14678  iuncld  14804  ssnei2  14846  topssnei  14851  restopnb  14870  cnfval  14883  cnpfval  14884  iscnp4  14907  cnptopco  14911  cncnpi  14917  cncnp  14919  cnconst2  14922  cnrest2  14925  cnptoprest  14928  cnptoprest2  14929  cnpdis  14931  lmss  14935  lmtopcnp  14939  neitx  14957  txcnp  14960  txrest  14965  txdis1cn  14967  txlm  14968  cnmpt21  14980  imasnopn  14988  xmetres2  15068  blvalps  15077  blval  15078  elbl2ps  15081  elbl2  15082  blhalf  15097  blssexps  15118  blssex  15119  ssblex  15120  blin2  15121  bdmetval  15189  xmetxp  15196  xmettx  15199  metcnpi3  15206  txmetcnp  15207  addcncntoplem  15250  fsumcncntop  15256  elcncf2  15263  mulc1cncf  15278  cncfco  15280  cncfmet  15281  cncfmptc  15285  mulcncf  15297  dedekindeulemub  15307  dedekindeulemloc  15308  dedekindeulemlu  15310  dedekindeu  15312  dedekindicclemub  15316  dedekindicclemloc  15317  dedekindicclemlu  15319  dedekindicclemicc  15321  dedekindicc  15322  ivthinclemlopn  15325  ivthinclemuopn  15327  dich0  15341  limcimo  15354  cnplimccntop  15359  limccnp2lem  15365  limccnp2cntop  15366  dvfvalap  15370  dveflem  15415  plycolemc  15447  plyco  15448  plyrecj  15452  reeff1olem  15460  reeff1oleme  15461  eflt  15464  sin0pilem2  15471  pilem3  15472  ioocosf1o  15543  cxplt  15605  cxple  15606  cxplt3  15609  apcxp2  15628  rprelogbmul  15644  rprelogbdiv  15646  logbgt0b  15655  logbgcd1irrap  15659  mpodvdsmulf1o  15679  fsumdvdsmul  15680  lgsdir2lem5  15726  lgsdi  15731  lgsne0  15732  gausslemma2dlem1f1o  15754  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem2  15776  lgsquad2  15777  2sqlem6  15814  2sqlem8  15817  2sqlem9  15818  2sqlem10  15819  upgredg  15957  usgredg4  16028  uspgredg2vlem  16033  vtxedgfi  16048  vtxlpfi  16049  iswlkg  16070  upgriswlkdc  16101  upgr2wlkdc  16116  clwwlkccatlem  16137  nnti  16415  pwtrufal  16422  pwf1oexmid  16424  sssneq  16427  qdencn  16455  cvgcmp2n  16461  trilpolemlt1  16469  trirec0  16472  redc0  16485  reap0  16486  cndcap  16487  nconstwlpolemgt0  16492  neap0mkv  16497  supfz  16499  inffz  16500