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  4024  reg2exmidlema  4566  reg3exmidlemwe  4611  nnsucpred  4649  iotam  5246  fvmptt  5649  fcof1  5826  fliftfun  5839  isotr  5859  riotass2  5900  acexmidlemab  5912  ovmpodf  6050  fnmpoovd  6268  1stconst  6274  2ndconst  6275  cnvf1olem  6277  f1od2  6288  smoiso  6355  tfrcldm  6416  tfrcl  6417  nntr2  6556  swoer  6615  erinxp  6663  ecopovsymg  6688  th3qlem1  6691  f1imaen2g  6847  pw2f1odclem  6890  mapdom1g  6903  fict  6924  fidifsnen  6926  dif1enen  6936  fiunsnnn  6937  fisbth  6939  findcard2d  6947  findcard2sd  6948  diffifi  6950  ac6sfi  6954  fimax2gtri  6957  nnwetri  6972  unsnfi  6975  unsnfidcex  6976  unsnfidcel  6977  fisseneq  6988  ssfirab  6990  fidcenumlemrk  7013  fidcenumlemr  7014  sbthlemi6  7021  sbthlemi8  7023  isbth  7026  fiuni  7037  supmaxti  7063  infminti  7086  ordiso2  7094  eldju2ndl  7131  eldju2ndr  7132  omp1eomlem  7153  difinfsnlem  7158  difinfinf  7160  ctmlemr  7167  ctssdccl  7170  nninfninc  7182  fodjum  7205  fodju0  7206  omniwomnimkv  7226  exmidfodomrlemrALT  7263  acfun  7267  exmidaclem  7268  netap  7314  exmidmotap  7321  ccfunen  7324  cc1  7325  cc2lem  7326  dfplpq2  7414  dfmpq2  7415  mulpipqqs  7433  distrnqg  7447  enq0sym  7492  enq0tr  7494  distrnq0  7519  prarloclem3  7557  genplt2i  7570  addlocpr  7596  prmuloc  7626  distrlem1prl  7642  distrlem1pru  7643  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  ltaprg  7679  prplnqu  7680  addextpr  7681  recexprlemdisj  7690  recexprlemloc  7691  aptiprleml  7699  aptiprlemu  7700  ltmprr  7702  archpr  7703  cauappcvgprlemopl  7706  cauappcvgprlemopu  7708  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlem1  7719  cauappcvgprlemlim  7721  caucvgprlemnkj  7726  caucvgprlemopl  7729  caucvgprlemopu  7731  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemnjltk  7751  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemopu  7759  caucvgprprlemdisj  7762  caucvgprprlemloc  7763  caucvgprprlemaddq  7768  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemex  7782  suplocexprlemub  7783  recexgt0sr  7833  mulgt0sr  7838  prsrriota  7848  suplocsrlem  7868  addcnsr  7894  mulcnsr  7895  mulcnsrec  7903  axmulcom  7931  rereceu  7949  axarch  7951  axcaucvglemres  7959  axpre-suploclemres  7961  lelttr  8108  ltletr  8109  addcan  8199  addcan2  8200  addsub4  8262  ltadd2  8438  le2add  8463  lt2add  8464  lt2sub  8479  le2sub  8480  eqord1  8502  rereim  8605  apreap  8606  apreim  8622  mulreim  8623  apcotr  8626  apadd1  8627  addext  8629  apneg  8630  mulext1  8631  mulext  8633  ltleap  8651  aprcl  8665  mulap0  8673  mulcanapd  8680  recapb  8690  rec11ap  8729  rec11rap  8730  divdivdivap  8732  ddcanap  8745  divadddivap  8746  prodgt0gt0  8870  prodgt0  8871  prodge0  8873  lemulge11  8885  lt2mul2div  8898  ltrec  8902  lerec  8903  lerec2  8908  ledivp1  8922  mulle0r  8963  nn0ge0div  9404  suprzclex  9415  qapne  9704  xrlelttr  9872  xrltletr  9873  xrre3  9888  xrrege0  9891  xaddge0  9944  xle2add  9945  xlt2add  9946  fzass4  10128  fzrev  10150  elfz1b  10156  eluzgtdifelfzo  10264  fzocatel  10266  exbtwnzlemex  10318  rebtwn2z  10323  modqid  10420  modqcyc  10430  modqaddabs  10433  modqaddmod  10434  mulqaddmodid  10435  modqadd2mod  10445  modqltm1p1mod  10447  modqsubmod  10453  modqsubmodmod  10454  modaddmodup  10458  modqmulmod  10460  modqmulmodr  10461  modqaddmulmod  10462  modqsubdir  10464  frec2uzisod  10478  uzennn  10507  iseqovex  10529  seqvalcd  10532  seq1g  10534  seqf  10535  seqovcd  10538  seqclg  10543  seqm1g  10545  seq3shft2  10552  seqshft2g  10553  monoord  10556  iseqf1olemnab  10572  seqf1oglem1  10590  seqf1og  10592  seqhomog  10601  seqfeq4g  10602  seq3distr  10603  expnegzap  10644  ltexp2a  10662  le2sq2  10686  bernneq  10731  expnlbnd2  10736  nn0ltexp2  10780  nn0opth2  10795  faclbnd  10812  bcval5  10834  hashcl  10852  hashen  10855  fihashdom  10874  hashunlem  10875  hashun  10876  hashxp  10897  fimaxq  10898  zfz1isolem1  10911  zfz1iso  10912  seq3coll  10913  sswrd  10923  cvg1nlemres  11129  cvg1n  11130  resqrexlemp1rp  11150  resqrexlemoverl  11165  resqrexlemex  11169  sqrtsq  11188  abslt  11232  absle  11233  abs3lem  11255  maxleastlt  11359  maxltsup  11362  fimaxre2  11370  negfi  11371  xrmaxleastlt  11399  xrmaxltsup  11401  xrmaxaddlem  11403  2clim  11444  climcn2  11452  addcn2  11453  mulcn2  11455  reccn2ap  11456  climge0  11468  climcau  11490  summodclem2  11525  summodc  11526  zsumdc  11527  fsumf1o  11533  fisumss  11535  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  mptfzshft  11585  fsumrev  11586  fsummulc2  11591  fsumconst  11597  modfsummod  11601  fsumrelem  11614  binom  11627  cvgratnn  11674  mertenslemub  11677  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodf1o  11731  fprodssdc  11733  fprodmul  11734  fprodcl2lem  11748  fprodrev  11762  fprodconst  11763  fprodap0  11764  fprodrec  11772  fprodap0f  11779  fprodle  11783  fprodmodd  11784  efcllem  11802  tanaddaplem  11881  moddvds  11942  dvdsflip  11993  oexpneg  12018  nn0o  12048  fldivndvdslt  12076  zsupcllemstep  12082  zsupcllemex  12083  zssinfcl  12085  suprzubdc  12089  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemeu  12144  dfgcd3  12147  dfgcd2  12151  dvdsmulgcd  12162  bezoutr  12169  nninfctlemfo  12177  lcmgcdlem  12215  coprmdvds2  12231  qredeu  12235  rpdvds  12237  cncongr1  12241  prmind2  12258  isprm5lem  12279  isprm6  12285  oddpwdclemdc  12311  nonsq  12345  hashdvds  12359  crth  12362  eulerthlemh  12369  prmdiveq  12374  hashgcdlem  12376  hashgcdeq  12377  nnnn0modprm0  12393  pclemub  12425  pceu  12433  pcmul  12439  pcqmul  12441  pcgcd1  12466  pc2dvds  12468  difsqpwdvds  12476  pcmpt  12481  prmpwdvds  12493  1arith  12505  mul4sq  12532  4sqlemafi  12533  4sqlemffi  12534  4sqexercise2  12537  ennnfonelemg  12560  ennnfonelemex  12571  ennnfonelemrnh  12573  ennnfonelemf1  12575  ennnfonelemrn  12576  ennnfonelemdm  12577  ennnfonelemim  12581  ennnfone  12582  ctinf  12587  ctiunctlemfo  12596  nninfdclemcl  12605  nninfdclemf  12606  nninfdclemp1  12607  unbendc  12611  isstruct2r  12629  setscom  12658  ercpbl  12914  opifismgmdc  12954  grpinvalem  12968  igsumvalx  12972  gsumfzval  12974  gsumval2  12980  sgrppropd  12996  mndpropd  13021  issubmnd  13023  submnd0  13025  mhmf1o  13042  subsubm  13055  0mhm  13058  resmhm  13059  mhmco  13062  mhmima  13063  mhmeql  13064  gsumfzz  13067  gsumwsubmcl  13068  gsumfzcl  13071  grprcan  13109  grpinvid1  13124  grpinvid2  13125  grplcan  13134  grplmulf1o  13146  grpnpncan0  13168  dfgrp3mlem  13170  grplactcnv  13174  mulgval  13192  mulgfng  13194  mulgnngsum  13197  mulg1  13199  mulgnnp1  13200  mulgneg  13210  mulgnndir  13221  mulgdirlem  13223  mulgnn0ass  13228  mulgass  13229  subgmulg  13258  issubg4m  13263  subsubg  13267  subgintm  13268  isnsg3  13277  eqgcpbl  13298  ghmeql  13337  ghmnsgima  13338  ghmnsgpreima  13339  ghmf1  13343  ghmf1o  13345  conjghm  13346  qusghm  13352  ablpncan3  13387  invghm  13399  eqgabl  13400  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  rngpropd  13451  imasrng  13452  qusrng  13454  srglmhm  13489  srgrmhm  13490  ringpropd  13534  ringlghm  13557  ringrghm  13558  imasring  13560  qusring2  13562  opprrngbg  13574  dvdsrvald  13589  dvdsrd  13590  dvdsrex  13594  dvdsrtr  13597  unitpropdg  13644  rhmopp  13672  isnzr2  13680  issubrng2  13706  subrngintm  13708  subsubrng  13710  subrgintm  13739  subsubrg  13741  rhmpropd  13750  aprap  13782  lmodprop2d  13844  rmodislmod  13847  lssvacl  13861  lssvsubcl  13862  lssvscl  13871  islss3  13875  lss1d  13879  rnglidlmcl  13976  2idlcpblrng  14019  crngridl  14026  expghmap  14095  mulgghm2  14096  mulgrhm  14097  znf1o  14139  znleval  14141  znidom  14145  znidomb  14146  znunit  14147  iuncld  14283  ssnei2  14325  topssnei  14330  restopnb  14349  cnfval  14362  cnpfval  14363  iscnp4  14386  cnptopco  14390  cncnpi  14396  cncnp  14398  cnconst2  14401  cnrest2  14404  cnptoprest  14407  cnptoprest2  14408  cnpdis  14410  lmss  14414  lmtopcnp  14418  neitx  14436  txcnp  14439  txrest  14444  txdis1cn  14446  txlm  14447  cnmpt21  14459  imasnopn  14467  xmetres2  14547  blvalps  14556  blval  14557  elbl2ps  14560  elbl2  14561  blhalf  14576  blssexps  14597  blssex  14598  ssblex  14599  blin2  14600  bdmetval  14668  xmetxp  14675  xmettx  14678  metcnpi3  14685  txmetcnp  14686  addcncntoplem  14719  fsumcncntop  14724  elcncf2  14729  mulc1cncf  14744  cncfco  14746  cncfmet  14747  cncfmptc  14750  mulcncf  14762  dedekindeulemub  14772  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeu  14777  dedekindicclemub  14781  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicclemicc  14786  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemuopn  14792  dich0  14806  limcimo  14819  cnplimccntop  14824  limccnp2lem  14830  limccnp2cntop  14831  dvfvalap  14835  dveflem  14872  reeff1olem  14906  reeff1oleme  14907  eflt  14910  sin0pilem2  14917  pilem3  14918  ioocosf1o  14989  cxplt  15050  cxple  15051  cxplt3  15054  apcxp2  15072  rprelogbmul  15087  rprelogbdiv  15089  logbgt0b  15098  logbgcd1irrap  15102  lgsdir2lem5  15148  lgsdi  15153  lgsne0  15154  gausslemma2dlem1f1o  15176  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem6  15207  2sqlem8  15210  2sqlem9  15211  2sqlem10  15212  nnti  15485  pwtrufal  15488  pwf1oexmid  15490  sssneq  15492  qdencn  15517  cvgcmp2n  15523  trilpolemlt1  15531  trirec0  15534  redc0  15547  reap0  15548  cndcap  15549  nconstwlpolemgt0  15554  neap0mkv  15559  supfz  15561  inffz  15562