Theorem simprr 500

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 476	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1rr  1012  simp2rr  1016  simp3rr  1020  disjiun  3862  reg2exmidlema  4378  reg3exmidlemwe  4422  fvmptt  5430  fcof1  5600  fliftfun  5613  isotr  5633  riotass2  5672  acexmidlemab  5684  ovmpt2df  5814  grprinvlem  5877  1stconst  6024  2ndconst  6025  cnvf1olem  6027  f1od2  6038  smoiso  6105  tfrcldm  6166  tfrcl  6167  swoer  6360  erinxp  6406  ecopovsymg  6431  th3qlem1  6434  f1imaen2g  6590  mapdom1g  6643  fict  6664  fidifsnen  6666  dif1enen  6676  fiunsnnn  6677  fisbth  6679  findcard2d  6687  findcard2sd  6688  diffifi  6690  ac6sfi  6694  fimax2gtri  6697  nnwetri  6706  unsnfi  6709  unsnfidcex  6710  unsnfidcel  6711  fisseneq  6722  ssfirab  6723  fidcenumlemrk  6743  fidcenumlemr  6744  sbthlemi6  6751  sbthlemi8  6753  isbth  6756  supmaxti  6779  infminti  6802  ordiso2  6808  eldju2ndl  6843  eldju2ndr  6844  ctmlemr  6870  fodjum  6889  fodju0  6890  exmidfodomrlemrALT  6926  dfplpq2  7010  dfmpq2  7011  mulpipqqs  7029  distrnqg  7043  enq0sym  7088  enq0tr  7090  distrnq0  7115  prarloclem3  7153  genplt2i  7166  addlocpr  7192  prmuloc  7222  distrlem1prl  7238  distrlem1pru  7239  ltexprlemopl  7257  ltexprlemopu  7259  ltexprlemfl  7265  ltexprlemrl  7266  ltexprlemfu  7267  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  ltaprg  7275  prplnqu  7276  addextpr  7277  recexprlemdisj  7286  recexprlemloc  7287  aptiprleml  7295  aptiprlemu  7296  ltmprr  7298  archpr  7299  cauappcvgprlemopl  7302  cauappcvgprlemopu  7304  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlem1  7315  cauappcvgprlemlim  7317  caucvgprlemnkj  7322  caucvgprlemopl  7325  caucvgprlemopu  7327  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprprlemnkltj  7345  caucvgprprlemnkeqj  7346  caucvgprprlemnjltk  7347  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemopu  7355  caucvgprprlemdisj  7358  caucvgprprlemloc  7359  caucvgprprlemaddq  7364  recexgt0sr  7416  mulgt0sr  7420  prsrriota  7430  addcnsr  7468  mulcnsr  7469  mulcnsrec  7477  axmulcom  7503  rereceu  7521  axarch  7523  axcaucvglemres  7531  lelttr  7670  ltletr  7671  addcan  7759  addcan2  7760  addsub4  7822  ltadd2  7994  le2add  8019  lt2add  8020  lt2sub  8035  le2sub  8036  eqord1  8058  rereim  8160  apreap  8161  apreim  8177  mulreim  8178  apcotr  8181  apadd1  8182  addext  8184  apneg  8185  mulext1  8186  mulext  8188  ltleap  8204  mulap0  8220  mulcanapd  8227  rec11ap  8274  rec11rap  8275  divdivdivap  8277  ddcanap  8290  divadddivap  8291  prodgt0gt0  8409  prodgt0  8410  prodge0  8412  lemulge11  8424  lt2mul2div  8437  ltrec  8441  lerec  8442  lerec2  8447  ledivp1  8461  mulle0r  8502  nn0ge0div  8932  suprzclex  8943  qapne  9223  xrlelttr  9372  xrltletr  9373  xrre3  9388  xrrege0  9391  xaddge0  9444  xle2add  9445  xlt2add  9446  fzass4  9625  fzrev  9647  elfz1b  9653  eluzgtdifelfzo  9757  fzocatel  9759  exbtwnzlemex  9810  rebtwn2z  9815  modqid  9905  modqcyc  9915  modqaddabs  9918  modqaddmod  9919  mulqaddmodid  9920  modqadd2mod  9930  modqltm1p1mod  9932  modqsubmod  9938  modqsubmodmod  9939  modaddmodup  9943  modqmulmod  9945  modqmulmodr  9946  modqaddmulmod  9947  modqsubdir  9949  frec2uzisod  9963  iseqovex  10016  iseqval  10017  iseqfclt  10025  seqf  10026  seq3shft2  10038  monoord  10042  iseqf1olemnab  10054  seq3distr  10079  expnegzap  10120  ltexp2a  10138  le2sq2  10161  bernneq  10205  expnlbnd2  10210  nn0opth2  10263  faclbnd  10280  bcval5  10302  hashcl  10320  hashen  10323  fihashdom  10342  hashunlem  10343  hashun  10344  hashxp  10365  fimaxq  10366  zfz1isolem1  10376  zfz1iso  10377  seq3coll  10378  cvg1nlemres  10549  cvg1n  10550  resqrexlemp1rp  10570  resqrexlemoverl  10585  resqrexlemex  10589  sqrtsq  10608  abslt  10652  absle  10653  abs3lem  10675  maxleastlt  10779  maxltsup  10782  fimaxre2  10789  negfi  10790  xrmaxleastlt  10815  xrmaxltsup  10817  xrmaxaddlem  10819  2clim  10860  climcn2  10868  addcn2  10869  mulcn2  10871  reccn2ap  10872  climge0  10884  climcau  10906  summodclem2  10941  summodc  10942  zsumdc  10943  fsumf1o  10949  fisumss  10951  fsum3cvg3  10955  fsumcl2lem  10957  fsumadd  10965  mptfzshft  11001  fsumrev  11002  fsummulc2  11007  fsumconst  11013  modfsummod  11017  fsumrelem  11030  binom  11043  cvgratnn  11090  mertenslemub  11093  efcllem  11114  tanaddaplem  11194  moddvds  11248  dvdsflip  11295  oexpneg  11320  nn0o  11350  fldivndvdslt  11378  zsupcllemstep  11384  zsupcllemex  11385  zssinfcl  11387  bezoutlemnewy  11428  bezoutlemstep  11429  bezoutlemeu  11439  dfgcd3  11442  dfgcd2  11446  dvdsmulgcd  11457  bezoutr  11464  lcmgcdlem  11502  coprmdvds2  11518  qredeu  11522  rpdvds  11524  cncongr1  11528  prmind2  11545  isprm6  11569  oddpwdclemdc  11594  nonsq  11628  hashdvds  11640  crth  11643  hashgcdlem  11646  hashgcdeq  11647  isstruct2r  11670  setscom  11699  iuncld  11983  ssnei2  12025  topssnei  12030  restopnb  12049  cnfval  12062  cnpfval  12063  iscnp4  12085  cnptopco  12089  cncnpi  12095  cncnp  12097  cnconst2  12100  cnrest2  12103  cnptoprest  12106  cnptoprest2  12107  cnpdis  12109  lmss  12113  lmtopcnp  12117  xmetres2  12181  blvalps  12190  blval  12191  elbl2ps  12194  elbl2  12195  blhalf  12210  blssexps  12231  blssex  12232  ssblex  12233  blin2  12234  bdmetval  12302  metcnpi3  12315  elcncf2  12343  mulc1cncf  12358  cncfco  12360  cncfmet  12361  cncfmptc  12362  mulcncf  12370  nnsucpred  12612  nnti  12613  qdencn  12636  supfz  12637  inffz  12638