Theorem simprl 521

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

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:  simp1rl  1047  simp2rl  1051  simp3rl  1055  rmob  3005  disjiun  3932  reg3exmidlemwe  4501  0xp  4627  imainss  4962  fvmptt  5520  fcof1o  5698  isotr  5725  riota5f  5762  ovmpodf  5910  grprinvlem  5973  grpridd  5975  unielxp  6080  fnmpoovd  6120  1stconst  6126  2ndconst  6127  cnvf1olem  6129  tfrlemi14d  6238  tfrexlem  6239  tfr1onlemres  6254  tfrcllemres  6267  tfrcldm  6268  frecabcl  6304  nnaordi  6412  swoer  6465  qliftfun  6519  ecopovsymg  6536  th3qlem1  6539  mapen  6748  mapxpen  6750  fidifsnen  6772  fisbth  6785  findcard2d  6793  findcard2sd  6794  diffisn  6795  diffifi  6796  ac6sfi  6800  fimax2gtri  6803  fientri3  6811  nnwetri  6812  unsnfi  6815  unsnfidcex  6816  unsnfidcel  6817  fisseneq  6828  fidcenumlemrk  6850  fidcenumlemr  6851  isbth  6863  ordiso2  6928  difinfsnlem  6992  difinfinf  6994  ctmlemr  7001  ctssdccl  7004  fodjum  7026  fodju0  7027  omniwomnimkv  7049  exmidfodomrlemrALT  7076  cc1  7097  cc2lem  7098  cc3  7100  cc4f  7101  cc4n  7103  dfplpq2  7186  dfmpq2  7187  mulpipqqs  7205  distrnqg  7219  ltexnqq  7240  subhalfnqq  7246  distrnq0  7291  prarloclemup  7327  prarloclem3  7329  prarloc  7335  genplt2i  7342  nqprl  7383  nqpru  7384  prmuloc  7398  mullocpr  7403  distrlem4prl  7416  distrlem4pru  7417  ltaddpr  7429  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  ltaprlem  7450  ltaprg  7451  prplnqu  7452  addextpr  7453  recexprlemdisj  7462  recexprlemloc  7463  recexprlem1ssl  7465  aptiprleml  7471  aptiprlemu  7472  ltmprr  7474  archpr  7475  cauappcvgprlemopl  7478  cauappcvgprlemopu  7480  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlem1  7491  cauappcvgprlem2  7492  cauappcvgprlemlim  7493  caucvgprlemnkj  7498  caucvgprlemopl  7501  caucvgprlemopu  7503  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlem2  7512  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnjltk  7523  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemopu  7531  caucvgprprlemdisj  7534  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  caucvgprprlemaddq  7540  caucvgprprlem2  7542  suplocexprlemrl  7549  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemex  7554  suplocexprlemub  7555  suplocexprlemlub  7556  recexgt0sr  7605  mulgt0sr  7610  prsrriota  7620  caucvgsrlemoffres  7632  suplocsrlem  7640  cnm  7664  addcnsr  7666  mulcnsr  7667  mulcnsrec  7675  axaddcl  7696  axmulcl  7698  axmulcom  7703  rereceu  7721  recriota  7722  axcaucvglemres  7731  axpre-suploclemres  7733  lelttr  7876  ltletr  7877  readdcan  7926  addcan  7966  addcan2  7967  addsub4  8029  ltadd2  8205  le2add  8230  lt2add  8231  lt2sub  8246  le2sub  8247  eqord1  8269  rimul  8371  rereim  8372  ltmul1  8378  apreim  8389  mulreim  8390  apcotr  8393  apadd1  8394  addext  8396  apneg  8397  mulext1  8398  mulext  8400  ltleap  8418  aprcl  8432  mulap0  8439  mulcanapd  8446  receuap  8454  rec11ap  8494  rec11rap  8495  divdivdivap  8497  ddcanap  8510  divadddivap  8511  conjmulap  8513  subrecap  8622  prodgt0gt0  8633  prodge0  8636  ltmul12a  8642  lemulge11  8648  lt2mul2div  8661  ltrec  8665  lerec  8666  lt2msq  8668  lerec2  8671  le2msq  8683  msq11  8684  ledivp1  8685  mulle0r  8726  suprzclex  9173  peano5uzti  9183  supinfneg  9417  infsupneg  9418  qapne  9458  xrlelttr  9619  xrltletr  9620  xrre  9633  xaddge0  9691  xle2add  9692  xlt2add  9693  divelunit  9815  fzass4  9873  fzocatel  10007  exbtwnzlemex  10058  rebtwn2z  10063  qbtwnre  10065  modqid  10153  modqcyc  10163  modqaddabs  10166  modqaddmod  10167  mulqaddmodid  10168  modqadd2mod  10178  modqltm1p1mod  10180  modqsubmod  10186  modqsubmodmod  10187  modqmulmod  10193  modqmulmodr  10194  modqaddmulmod  10195  modqsubdir  10197  frec2uzisod  10211  iseqovex  10260  seqvalcd  10263  seqf  10265  seqovcd  10267  seq3fveq2  10273  seq3shft2  10277  monoord  10280  seq3split  10283  iseqf1olemnab  10292  seq3id2  10313  seq3distr  10317  expcl2lemap  10336  expnegzap  10358  ltexp2a  10376  le2sq2  10399  nn0opth2  10502  bcval5  10541  hashcl  10559  hashen  10562  fihashdom  10581  hashunlem  10582  hashun  10583  fimaxq  10605  zfz1isolem1  10615  zfz1iso  10616  cvg1nlemres  10789  cvg1n  10790  recvguniq  10799  resqrexlemp1rp  10810  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemex  10829  sqrtmul  10839  sqrtsq  10848  absexpzap  10884  absle  10893  abs3lem  10915  amgm2  10922  maxleastlt  11019  maxltsup  11022  fimaxre2  11030  xrmaxleastlt  11057  xrmaxltsup  11059  xrmaxaddlem  11061  climcn2  11110  addcn2  11111  mulcn2  11113  reccn2ap  11114  climcau  11148  summodclem2  11183  summodc  11184  fsumf1o  11191  fisumss  11193  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  fsum2dlemstep  11235  mptfzshft  11243  fsumrev  11244  fsummulc2  11249  modfsummod  11259  fsumrelem  11272  binom  11285  cvgratnn  11332  mertenslemub  11335  prodmodc  11379  zproddc  11380  efcllem  11402  tanaddaplem  11481  dvdsval2  11532  moddvds  11538  dvdsabseq  11581  dvdsflip  11585  oexpneg  11610  fldivndvdslt  11668  zsupcllemstep  11674  zssinfcl  11677  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemeu  11731  dfgcd3  11734  bezout  11735  dvdsmulgcd  11749  bezoutr  11756  ialgrlem1st  11759  lcmgcdlem  11794  coprmdvds2  11810  qredeu  11814  rpdvds  11816  isprm6  11861  pw2dvdslemn  11879  nonsq  11921  crth  11936  ennnfonelemg  11952  ennnfonelemex  11963  ennnfonelemrnh  11965  ennnfonelemrn  11968  ennnfonelemdm  11969  ennnfonelemnn0  11971  ennnfonelemim  11973  ennnfone  11974  ctinfomlemom  11976  ctinf  11979  ctiunctlemfo  11988  isstruct2r  12009  setscom  12038  epttop  12298  topssnei  12370  restbasg  12376  restopnb  12389  cnfval  12402  cnpfval  12403  iscnp4  12426  cnpnei  12427  cnptopco  12430  cncnp  12438  cnrest2  12444  cnptoprest  12447  cnptoprest2  12448  lmss  12454  lmtopcnp  12458  neitx  12476  txcnp  12479  txrest  12484  txdis  12485  txlm  12487  cnmpt21  12499  imasnopn  12507  xmetres2  12587  blvalps  12596  blval  12597  bl2in  12611  blhalf  12616  blssps  12635  blss  12636  blssexps  12637  blssex  12638  ssblex  12639  blin2  12640  metss2lem  12705  bdmetval  12708  bdmopn  12712  metrest  12714  xmetxp  12715  xmetxpbl  12716  xmettx  12718  metcnp3  12719  txmetcnp  12726  addcncntoplem  12759  elcncf2  12769  mulc1cncf  12784  cncfco  12786  cncfmet  12787  mulcncf  12799  dedekindeulemub  12804  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeu  12809  suplociccex  12811  dedekindicclemub  12813  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthdec  12830  limcimolemlt  12841  limcimo  12842  cnplimccntop  12847  limccnp2lem  12853  limccnp2cntop  12854  dvfvalap  12858  dveflem  12895  reeff1olem  12900  reeff1oleme  12901  eflt  12904  sin0pilem2  12911  pilem3  12912  ptolemy  12953  ioocosf1o  12983  cxplt  13044  cxple  13045  cxplt3  13048  apcxp2  13066  rprelogbmul  13080  rprelogbdiv  13082  logbgt0b  13091  logbgcd1irrap  13095  nnti  13362  pwtrufal  13365  pwf1oexmid  13367  sssneq  13370  qdencn  13397  cvgcmp2n  13403  trilpolemlt1  13409  trirec0  13412  trirec0xor  13413  supfz  13428  inffz  13429