Theorem simprr 527

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 488	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  1058  simp2rr  1062  simp3rr  1066  disjiun  3984  reg2exmidlema  4518  reg3exmidlemwe  4563  nnsucpred  4601  iotam  5190  fvmptt  5587  fcof1  5762  fliftfun  5775  isotr  5795  riotass2  5835  acexmidlemab  5847  ovmpodf  5984  fnmpoovd  6194  1stconst  6200  2ndconst  6201  cnvf1olem  6203  f1od2  6214  smoiso  6281  tfrcldm  6342  tfrcl  6343  nntr2  6482  swoer  6541  erinxp  6587  ecopovsymg  6612  th3qlem1  6615  f1imaen2g  6771  mapdom1g  6825  fict  6846  fidifsnen  6848  dif1enen  6858  fiunsnnn  6859  fisbth  6861  findcard2d  6869  findcard2sd  6870  diffifi  6872  ac6sfi  6876  fimax2gtri  6879  nnwetri  6893  unsnfi  6896  unsnfidcex  6897  unsnfidcel  6898  fisseneq  6909  ssfirab  6911  fidcenumlemrk  6931  fidcenumlemr  6932  sbthlemi6  6939  sbthlemi8  6941  isbth  6944  fiuni  6955  supmaxti  6981  infminti  7004  ordiso2  7012  eldju2ndl  7049  eldju2ndr  7050  omp1eomlem  7071  difinfsnlem  7076  difinfinf  7078  ctmlemr  7085  ctssdccl  7088  fodjum  7122  fodju0  7123  omniwomnimkv  7143  exmidfodomrlemrALT  7180  acfun  7184  exmidaclem  7185  ccfunen  7226  cc1  7227  cc2lem  7228  dfplpq2  7316  dfmpq2  7317  mulpipqqs  7335  distrnqg  7349  enq0sym  7394  enq0tr  7396  distrnq0  7421  prarloclem3  7459  genplt2i  7472  addlocpr  7498  prmuloc  7528  distrlem1prl  7544  distrlem1pru  7545  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  ltaprg  7581  prplnqu  7582  addextpr  7583  recexprlemdisj  7592  recexprlemloc  7593  aptiprleml  7601  aptiprlemu  7602  ltmprr  7604  archpr  7605  cauappcvgprlemopl  7608  cauappcvgprlemopu  7610  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlem1  7621  cauappcvgprlemlim  7623  caucvgprlemnkj  7628  caucvgprlemopl  7631  caucvgprlemopu  7633  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnjltk  7653  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemopu  7661  caucvgprprlemdisj  7664  caucvgprprlemloc  7665  caucvgprprlemaddq  7670  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemex  7684  suplocexprlemub  7685  recexgt0sr  7735  mulgt0sr  7740  prsrriota  7750  suplocsrlem  7770  addcnsr  7796  mulcnsr  7797  mulcnsrec  7805  axmulcom  7833  rereceu  7851  axarch  7853  axcaucvglemres  7861  axpre-suploclemres  7863  lelttr  8008  ltletr  8009  addcan  8099  addcan2  8100  addsub4  8162  ltadd2  8338  le2add  8363  lt2add  8364  lt2sub  8379  le2sub  8380  eqord1  8402  rereim  8505  apreap  8506  apreim  8522  mulreim  8523  apcotr  8526  apadd1  8527  addext  8529  apneg  8530  mulext1  8531  mulext  8533  ltleap  8551  aprcl  8565  mulap0  8572  mulcanapd  8579  rec11ap  8627  rec11rap  8628  divdivdivap  8630  ddcanap  8643  divadddivap  8644  prodgt0gt0  8767  prodgt0  8768  prodge0  8770  lemulge11  8782  lt2mul2div  8795  ltrec  8799  lerec  8800  lerec2  8805  ledivp1  8819  mulle0r  8860  nn0ge0div  9299  suprzclex  9310  qapne  9598  xrlelttr  9763  xrltletr  9764  xrre3  9779  xrrege0  9782  xaddge0  9835  xle2add  9836  xlt2add  9837  fzass4  10018  fzrev  10040  elfz1b  10046  eluzgtdifelfzo  10153  fzocatel  10155  exbtwnzlemex  10206  rebtwn2z  10211  modqid  10305  modqcyc  10315  modqaddabs  10318  modqaddmod  10319  mulqaddmodid  10320  modqadd2mod  10330  modqltm1p1mod  10332  modqsubmod  10338  modqsubmodmod  10339  modaddmodup  10343  modqmulmod  10345  modqmulmodr  10346  modqaddmulmod  10347  modqsubdir  10349  frec2uzisod  10363  uzennn  10392  iseqovex  10412  seqvalcd  10415  seqf  10417  seqovcd  10419  seq3shft2  10429  monoord  10432  iseqf1olemnab  10444  seq3distr  10469  expnegzap  10510  ltexp2a  10528  le2sq2  10551  bernneq  10596  expnlbnd2  10601  nn0ltexp2  10644  nn0opth2  10658  faclbnd  10675  bcval5  10697  hashcl  10715  hashen  10718  fihashdom  10738  hashunlem  10739  hashun  10740  hashxp  10761  fimaxq  10762  zfz1isolem1  10775  zfz1iso  10776  seq3coll  10777  cvg1nlemres  10949  cvg1n  10950  resqrexlemp1rp  10970  resqrexlemoverl  10985  resqrexlemex  10989  sqrtsq  11008  abslt  11052  absle  11053  abs3lem  11075  maxleastlt  11179  maxltsup  11182  fimaxre2  11190  negfi  11191  xrmaxleastlt  11219  xrmaxltsup  11221  xrmaxaddlem  11223  2clim  11264  climcn2  11272  addcn2  11273  mulcn2  11275  reccn2ap  11276  climge0  11288  climcau  11310  summodclem2  11345  summodc  11346  zsumdc  11347  fsumf1o  11353  fisumss  11355  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  mptfzshft  11405  fsumrev  11406  fsummulc2  11411  fsumconst  11417  modfsummod  11421  fsumrelem  11434  binom  11447  cvgratnn  11494  mertenslemub  11497  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodf1o  11551  fprodssdc  11553  fprodmul  11554  fprodcl2lem  11568  fprodrev  11582  fprodconst  11583  fprodap0  11584  fprodrec  11592  fprodap0f  11599  fprodle  11603  fprodmodd  11604  efcllem  11622  tanaddaplem  11701  moddvds  11761  dvdsflip  11811  oexpneg  11836  nn0o  11866  fldivndvdslt  11894  zsupcllemstep  11900  zsupcllemex  11901  zssinfcl  11903  suprzubdc  11907  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemeu  11962  dfgcd3  11965  dfgcd2  11969  dvdsmulgcd  11980  bezoutr  11987  lcmgcdlem  12031  coprmdvds2  12047  qredeu  12051  rpdvds  12053  cncongr1  12057  prmind2  12074  isprm5lem  12095  isprm6  12101  oddpwdclemdc  12127  nonsq  12161  hashdvds  12175  crth  12178  eulerthlemh  12185  prmdiveq  12190  hashgcdlem  12192  hashgcdeq  12193  nnnn0modprm0  12209  pclemub  12241  pceu  12249  pcmul  12255  pcqmul  12257  pcgcd1  12281  pc2dvds  12283  difsqpwdvds  12291  pcmpt  12295  prmpwdvds  12307  1arith  12319  mul4sq  12346  ennnfonelemg  12358  ennnfonelemex  12369  ennnfonelemrnh  12371  ennnfonelemf1  12373  ennnfonelemrn  12374  ennnfonelemdm  12375  ennnfonelemim  12379  ennnfone  12380  ctinf  12385  ctiunctlemfo  12394  nninfdclemcl  12403  nninfdclemf  12404  nninfdclemp1  12405  unbendc  12409  isstruct2r  12427  setscom  12456  opifismgmdc  12625  grprinvlem  12639  mndpropd  12676  mhmf1o  12693  0mhm  12704  mhmco  12705  mhmima  12706  mhmeql  12707  grprcan  12740  grpinvid1  12754  grpinvid2  12755  grplcan  12761  iuncld  12909  ssnei2  12951  topssnei  12956  restopnb  12975  cnfval  12988  cnpfval  12989  iscnp4  13012  cnptopco  13016  cncnpi  13022  cncnp  13024  cnconst2  13027  cnrest2  13030  cnptoprest  13033  cnptoprest2  13034  cnpdis  13036  lmss  13040  lmtopcnp  13044  neitx  13062  txcnp  13065  txrest  13070  txdis1cn  13072  txlm  13073  cnmpt21  13085  imasnopn  13093  xmetres2  13173  blvalps  13182  blval  13183  elbl2ps  13186  elbl2  13187  blhalf  13202  blssexps  13223  blssex  13224  ssblex  13225  blin2  13226  bdmetval  13294  xmetxp  13301  xmettx  13304  metcnpi3  13311  txmetcnp  13312  addcncntoplem  13345  fsumcncntop  13350  elcncf2  13355  mulc1cncf  13370  cncfco  13372  cncfmet  13373  cncfmptc  13376  mulcncf  13385  dedekindeulemub  13390  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeu  13395  dedekindicclemub  13399  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicclemicc  13404  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemuopn  13410  limcimo  13428  cnplimccntop  13433  limccnp2lem  13439  limccnp2cntop  13440  dvfvalap  13444  dveflem  13481  reeff1olem  13486  reeff1oleme  13487  eflt  13490  sin0pilem2  13497  pilem3  13498  ioocosf1o  13569  cxplt  13630  cxple  13631  cxplt3  13634  apcxp2  13652  rprelogbmul  13667  rprelogbdiv  13669  logbgt0b  13678  logbgcd1irrap  13682  lgsdir2lem5  13727  lgsdi  13732  lgsne0  13733  2sqlem6  13750  2sqlem8  13753  2sqlem9  13754  2sqlem10  13755  nnti  14027  pwtrufal  14030  pwf1oexmid  14032  sssneq  14035  qdencn  14059  cvgcmp2n  14065  trilpolemlt1  14073  trirec0  14076  redc0  14089  reap0  14090  nconstwlpolemgt0  14095  supfz  14100  inffz  14101