Theorem simprl 483

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprl	|- ( ( ph /\ ( ps /\ ch ) ) -> ps )

Proof of Theorem simprl

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2	1	ad2antrl 459	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  simp1rl  969  simp2rl  973  simp3rl  977  rmob  2850  reg3exmidlemwe  4303  0xp  4420  imainss  4739  fvmptt  5262  fcof1o  5429  isotr  5456  riota5f  5492  ovmpt2df  5632  grprinvlem  5695  grpridd  5697  unielxp  5800  1stconst  5842  2ndconst  5843  cnvf1olem  5845  tfrlemi14d  5947  tfrexlem  5948  nnaordi  6081  swoer  6134  qliftfun  6188  ecopovsymg  6205  th3qlem1  6208  fidifsnen  6331  fisbth  6340  findcard2d  6348  findcard2sd  6349  diffisn  6350  diffifi  6351  ac6sfi  6352  fientri3  6353  nnwetri  6354  ordiso2  6357  dfplpq2  6452  dfmpq2  6453  mulpipqqs  6471  distrnqg  6485  ltexnqq  6506  subhalfnqq  6512  distrnq0  6557  prarloclemup  6593  prarloclem3  6595  prarloc  6601  genplt2i  6608  nqprl  6649  nqpru  6650  prmuloc  6664  mullocpr  6669  distrlem4prl  6682  distrlem4pru  6683  ltaddpr  6695  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  ltaprlem  6716  ltaprg  6717  prplnqu  6718  addextpr  6719  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  aptiprleml  6737  aptiprlemu  6738  ltmprr  6740  archpr  6741  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlem1  6757  cauappcvgprlem2  6758  cauappcvgprlemlim  6759  caucvgprlemnkj  6764  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlem2  6778  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemdisj  6800  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemaddq  6806  caucvgprprlem2  6808  recexgt0sr  6858  mulgt0sr  6862  prsrriota  6872  caucvgsrlemoffres  6884  addcnsr  6910  mulcnsr  6911  mulcnsrec  6919  axaddcl  6940  axmulcl  6942  axmulcom  6945  rereceu  6963  recriota  6964  axcaucvglemres  6973  lelttr  7106  ltletr  7107  readdcan  7153  addcan  7191  addcan2  7192  addsub4  7254  ltadd2  7416  le2add  7439  lt2add  7440  lt2sub  7455  le2sub  7456  rimul  7576  rereim  7577  ltmul1  7583  apreim  7594  mulreim  7595  apcotr  7598  apadd1  7599  addext  7601  apneg  7602  mulext1  7603  mulext  7605  ltleap  7621  mulap0  7635  mulcanapd  7642  receuap  7650  rec11ap  7686  rec11rap  7687  divdivdivap  7689  ddcanap  7702  divadddivap  7703  conjmulap  7705  prodgt0gt0  7817  prodge0  7820  ltmul12a  7826  lemulge11  7832  lt2mul2div  7845  ltrec  7849  lerec  7850  lt2msq  7852  lerec2  7855  le2msq  7867  msq11  7868  ledivp1  7869  peano5uzti  8346  qapne  8574  xrlelttr  8722  xrltletr  8723  xrre  8733  divelunit  8870  fzass4  8925  fzocatel  9055  qbtwnzlemex  9105  rebtwn2z  9109  qbtwnre  9111  frec2uzisod  9193  iseqovex  9219  iseqval  9220  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  iseqdistr  9249  expivallem  9256  expcl2lemap  9267  expnegzap  9289  ltexp2a  9306  le2sq2  9329  cvg1nlemres  9584  cvg1n  9585  recvguniq  9593  resqrexlemp1rp  9604  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemex  9623  sqrtmul  9633  sqrtsq  9642  absexpzap  9676  absle  9685  abs3lem  9707  amgm2  9714  climcn2  9830  addcn2  9831  mulcn2  9833  climcau  9866  ialgrlem1st  9881  qdencn  10124