Theorem simprl 526

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 487	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  1057  simp2rl  1061  simp3rl  1065  rmob  3047  disjiun  3984  reg3exmidlemwe  4563  0xp  4691  imainss  5026  iotam  5190  fvmptt  5587  fcof1o  5768  isotr  5795  riota5f  5833  ovmpodf  5984  unielxp  6153  fnmpoovd  6194  1stconst  6200  2ndconst  6201  cnvf1olem  6203  tfrlemi14d  6312  tfrexlem  6313  tfr1onlemres  6328  tfrcllemres  6341  tfrcldm  6342  frecabcl  6378  nnaordi  6487  swoer  6541  qliftfun  6595  ecopovsymg  6612  th3qlem1  6615  mapen  6824  mapxpen  6826  fidifsnen  6848  fisbth  6861  findcard2d  6869  findcard2sd  6870  diffisn  6871  diffifi  6872  ac6sfi  6876  fimax2gtri  6879  fientri3  6892  nnwetri  6893  unsnfi  6896  unsnfidcex  6897  unsnfidcel  6898  fisseneq  6909  fidcenumlemrk  6931  fidcenumlemr  6932  isbth  6944  ordiso2  7012  difinfsnlem  7076  difinfinf  7078  ctmlemr  7085  ctssdccl  7088  fodjum  7122  fodju0  7123  omniwomnimkv  7143  exmidfodomrlemrALT  7180  cc1  7227  cc2lem  7228  cc3  7230  cc4f  7231  cc4n  7233  dfplpq2  7316  dfmpq2  7317  mulpipqqs  7335  distrnqg  7349  ltexnqq  7370  subhalfnqq  7376  distrnq0  7421  prarloclemup  7457  prarloclem3  7459  prarloc  7465  genplt2i  7472  nqprl  7513  nqpru  7514  prmuloc  7528  mullocpr  7533  distrlem4prl  7546  distrlem4pru  7547  ltaddpr  7559  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  ltaprlem  7580  ltaprg  7581  prplnqu  7582  addextpr  7583  recexprlemdisj  7592  recexprlemloc  7593  recexprlem1ssl  7595  aptiprleml  7601  aptiprlemu  7602  ltmprr  7604  archpr  7605  cauappcvgprlemopl  7608  cauappcvgprlemopu  7610  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlem1  7621  cauappcvgprlem2  7622  cauappcvgprlemlim  7623  caucvgprlemnkj  7628  caucvgprlemopl  7631  caucvgprlemopu  7633  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlem2  7642  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnjltk  7653  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemopu  7661  caucvgprprlemdisj  7664  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  caucvgprprlemaddq  7670  caucvgprprlem2  7672  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemex  7684  suplocexprlemub  7685  suplocexprlemlub  7686  recexgt0sr  7735  mulgt0sr  7740  prsrriota  7750  caucvgsrlemoffres  7762  suplocsrlem  7770  cnm  7794  addcnsr  7796  mulcnsr  7797  mulcnsrec  7805  axaddcl  7826  axmulcl  7828  axmulcom  7833  rereceu  7851  recriota  7852  axcaucvglemres  7861  axpre-suploclemres  7863  lelttr  8008  ltletr  8009  readdcan  8059  addcan  8099  addcan2  8100  addsub4  8162  ltadd2  8338  le2add  8363  lt2add  8364  lt2sub  8379  le2sub  8380  eqord1  8402  rimul  8504  rereim  8505  ltmul1  8511  apreim  8522  mulreim  8523  apcotr  8526  apadd1  8527  addext  8529  apneg  8530  mulext1  8531  mulext  8533  ltleap  8551  aprcl  8565  mulap0  8572  mulcanapd  8579  receuap  8587  rec11ap  8627  rec11rap  8628  divdivdivap  8630  ddcanap  8643  divadddivap  8644  conjmulap  8646  subrecap  8756  prodgt0gt0  8767  prodge0  8770  ltmul12a  8776  lemulge11  8782  lt2mul2div  8795  ltrec  8799  lerec  8800  lt2msq  8802  lerec2  8805  le2msq  8817  msq11  8818  ledivp1  8819  mulle0r  8860  suprzclex  9310  peano5uzti  9320  supinfneg  9554  infsupneg  9555  qapne  9598  xrlelttr  9763  xrltletr  9764  xrre  9777  xaddge0  9835  xle2add  9836  xlt2add  9837  divelunit  9959  fzass4  10018  fzocatel  10155  exbtwnzlemex  10206  rebtwn2z  10211  qbtwnre  10213  modqid  10305  modqcyc  10315  modqaddabs  10318  modqaddmod  10319  mulqaddmodid  10320  modqadd2mod  10330  modqltm1p1mod  10332  modqsubmod  10338  modqsubmodmod  10339  modqmulmod  10345  modqmulmodr  10346  modqaddmulmod  10347  modqsubdir  10349  frec2uzisod  10363  iseqovex  10412  seqvalcd  10415  seqf  10417  seqovcd  10419  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  iseqf1olemnab  10444  seq3id2  10465  seq3distr  10469  expcl2lemap  10488  expnegzap  10510  ltexp2a  10528  le2sq2  10551  nn0ltexp2  10644  nn0opth2  10658  bcval5  10697  hashcl  10715  hashen  10718  fihashdom  10738  hashunlem  10739  hashun  10740  fimaxq  10762  zfz1isolem1  10775  zfz1iso  10776  cvg1nlemres  10949  cvg1n  10950  recvguniq  10959  resqrexlemp1rp  10970  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemex  10989  sqrtmul  10999  sqrtsq  11008  absexpzap  11044  absle  11053  abs3lem  11075  amgm2  11082  maxleastlt  11179  maxltsup  11182  fimaxre2  11190  xrmaxleastlt  11219  xrmaxltsup  11221  xrmaxaddlem  11223  climcn2  11272  addcn2  11273  mulcn2  11275  reccn2ap  11276  climcau  11310  summodclem2  11345  summodc  11346  fsumf1o  11353  fisumss  11355  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  fsum2dlemstep  11397  mptfzshft  11405  fsumrev  11406  fsummulc2  11411  modfsummod  11421  fsumrelem  11434  binom  11447  cvgratnn  11494  mertenslemub  11497  prodmodc  11541  zproddc  11542  fprodf1o  11551  fprodssdc  11553  fprodmul  11554  fprodrev  11582  fprod2dlemstep  11585  efcllem  11622  tanaddaplem  11701  dvdsval2  11752  moddvds  11761  dvdsabseq  11807  dvdsflip  11811  oexpneg  11836  fldivndvdslt  11894  zsupcllemstep  11900  zssinfcl  11903  suprzubdc  11907  zsupssdc  11909  suprzcl2dc  11910  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemeu  11962  dfgcd3  11965  bezout  11966  dvdsmulgcd  11980  bezoutr  11987  ialgrlem1st  11996  lcmgcdlem  12031  coprmdvds2  12047  qredeu  12051  rpdvds  12053  isprm5lem  12095  isprm6  12101  pw2dvdslemn  12119  nonsq  12161  crth  12178  eulerthlemh  12185  pclemdc  12242  pcprendvds2  12245  pceu  12249  pcval  12250  pczpre  12251  pcmul  12255  pcqmul  12257  pcqcl  12260  pcid  12277  pcneg  12278  pcgcd1  12281  pc2dvds  12283  pcprmpw2  12286  difsqpwdvds  12291  pcmpt  12295  pockthg  12309  1arith  12319  mul4sq  12346  ennnfonelemg  12358  ennnfonelemex  12369  ennnfonelemrnh  12371  ennnfonelemrn  12374  ennnfonelemdm  12375  ennnfonelemnn0  12377  ennnfonelemim  12379  ennnfone  12380  ctinfomlemom  12382  ctinf  12385  ctiunctlemfo  12394  nninfdclemcl  12403  nninfdclemf  12404  nninfdclemp1  12405  unbendc  12409  isstruct2r  12427  setscom  12456  opifismgmdc  12625  grprinvlem  12639  grpridd  12641  mndpropd  12676  mhmf1o  12693  0mhm  12704  mhmco  12705  mhmima  12706  mhmeql  12707  grppropd  12724  grpinvid1  12754  grpinvid2  12755  grplcan  12761  epttop  12884  topssnei  12956  restbasg  12962  restopnb  12975  cnfval  12988  cnpfval  12989  iscnp4  13012  cnpnei  13013  cnptopco  13016  cncnp  13024  cnrest2  13030  cnptoprest  13033  cnptoprest2  13034  lmss  13040  lmtopcnp  13044  neitx  13062  txcnp  13065  txrest  13070  txdis  13071  txlm  13073  cnmpt21  13085  imasnopn  13093  xmetres2  13173  blvalps  13182  blval  13183  bl2in  13197  blhalf  13202  blssps  13221  blss  13222  blssexps  13223  blssex  13224  ssblex  13225  blin2  13226  metss2lem  13291  bdmetval  13294  bdmopn  13298  metrest  13300  xmetxp  13301  xmetxpbl  13302  xmettx  13304  metcnp3  13305  txmetcnp  13312  addcncntoplem  13345  elcncf2  13355  mulc1cncf  13370  cncfco  13372  cncfmet  13373  mulcncf  13385  dedekindeulemub  13390  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeu  13395  suplociccex  13397  dedekindicclemub  13399  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthdec  13416  limcimolemlt  13427  limcimo  13428  cnplimccntop  13433  limccnp2lem  13439  limccnp2cntop  13440  dvfvalap  13444  dveflem  13481  reeff1olem  13486  reeff1oleme  13487  eflt  13490  sin0pilem2  13497  pilem3  13498  ptolemy  13539  ioocosf1o  13569  cxplt  13630  cxple  13631  cxplt3  13634  apcxp2  13652  rprelogbmul  13667  rprelogbdiv  13669  logbgt0b  13678  logbgcd1irrap  13682  lgsdir2lem5  13727  lgsdir  13730  lgsdi  13732  lgsne0  13733  2sqlem6  13750  2sqlem10  13755  nnti  14027  pwtrufal  14030  pwf1oexmid  14032  sssneq  14035  qdencn  14059  cvgcmp2n  14065  trilpolemlt1  14073  trirec0  14076  trirec0xor  14077  redc0  14089  reap0  14090  nconstwlpolemgt0  14095  supfz  14100  inffz  14101