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  3982  reg3exmidlemwe  4561  0xp  4689  imainss  5024  iotam  5188  fvmptt  5585  fcof1o  5765  isotr  5792  riota5f  5830  ovmpodf  5981  unielxp  6150  fnmpoovd  6191  1stconst  6197  2ndconst  6198  cnvf1olem  6200  tfrlemi14d  6309  tfrexlem  6310  tfr1onlemres  6325  tfrcllemres  6338  tfrcldm  6339  frecabcl  6375  nnaordi  6484  swoer  6537  qliftfun  6591  ecopovsymg  6608  th3qlem1  6611  mapen  6820  mapxpen  6822  fidifsnen  6844  fisbth  6857  findcard2d  6865  findcard2sd  6866  diffisn  6867  diffifi  6868  ac6sfi  6872  fimax2gtri  6875  fientri3  6888  nnwetri  6889  unsnfi  6892  unsnfidcex  6893  unsnfidcel  6894  fisseneq  6905  fidcenumlemrk  6927  fidcenumlemr  6928  isbth  6940  ordiso2  7008  difinfsnlem  7072  difinfinf  7074  ctmlemr  7081  ctssdccl  7084  fodjum  7118  fodju0  7119  omniwomnimkv  7139  exmidfodomrlemrALT  7167  cc1  7214  cc2lem  7215  cc3  7217  cc4f  7218  cc4n  7220  dfplpq2  7303  dfmpq2  7304  mulpipqqs  7322  distrnqg  7336  ltexnqq  7357  subhalfnqq  7363  distrnq0  7408  prarloclemup  7444  prarloclem3  7446  prarloc  7452  genplt2i  7459  nqprl  7500  nqpru  7501  prmuloc  7515  mullocpr  7520  distrlem4prl  7533  distrlem4pru  7534  ltaddpr  7546  ltexprlemopl  7550  ltexprlemlol  7551  ltexprlemopu  7552  ltexprlemupu  7553  ltexprlemrl  7559  ltexprlemru  7561  addcanprleml  7563  addcanprlemu  7564  ltaprlem  7567  ltaprg  7568  prplnqu  7569  addextpr  7570  recexprlemdisj  7579  recexprlemloc  7580  recexprlem1ssl  7582  aptiprleml  7588  aptiprlemu  7589  ltmprr  7591  archpr  7592  cauappcvgprlemopl  7595  cauappcvgprlemopu  7597  cauappcvgprlemdisj  7600  cauappcvgprlemloc  7601  cauappcvgprlem1  7608  cauappcvgprlem2  7609  cauappcvgprlemlim  7610  caucvgprlemnkj  7615  caucvgprlemopl  7618  caucvgprlemopu  7620  caucvgprlemdisj  7623  caucvgprlemloc  7624  caucvgprlem2  7629  caucvgprprlemnkltj  7638  caucvgprprlemnkeqj  7639  caucvgprprlemnjltk  7640  caucvgprprlemmu  7644  caucvgprprlemopl  7646  caucvgprprlemopu  7648  caucvgprprlemdisj  7651  caucvgprprlemloc  7652  caucvgprprlemexbt  7655  caucvgprprlemaddq  7657  caucvgprprlem2  7659  suplocexprlemrl  7666  suplocexprlemmu  7667  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  suplocexprlemex  7671  suplocexprlemub  7672  suplocexprlemlub  7673  recexgt0sr  7722  mulgt0sr  7727  prsrriota  7737  caucvgsrlemoffres  7749  suplocsrlem  7757  cnm  7781  addcnsr  7783  mulcnsr  7784  mulcnsrec  7792  axaddcl  7813  axmulcl  7815  axmulcom  7820  rereceu  7838  recriota  7839  axcaucvglemres  7848  axpre-suploclemres  7850  lelttr  7995  ltletr  7996  readdcan  8046  addcan  8086  addcan2  8087  addsub4  8149  ltadd2  8325  le2add  8350  lt2add  8351  lt2sub  8366  le2sub  8367  eqord1  8389  rimul  8491  rereim  8492  ltmul1  8498  apreim  8509  mulreim  8510  apcotr  8513  apadd1  8514  addext  8516  apneg  8517  mulext1  8518  mulext  8520  ltleap  8538  aprcl  8552  mulap0  8559  mulcanapd  8566  receuap  8574  rec11ap  8614  rec11rap  8615  divdivdivap  8617  ddcanap  8630  divadddivap  8631  conjmulap  8633  subrecap  8743  prodgt0gt0  8754  prodge0  8757  ltmul12a  8763  lemulge11  8769  lt2mul2div  8782  ltrec  8786  lerec  8787  lt2msq  8789  lerec2  8792  le2msq  8804  msq11  8805  ledivp1  8806  mulle0r  8847  suprzclex  9297  peano5uzti  9307  supinfneg  9541  infsupneg  9542  qapne  9585  xrlelttr  9750  xrltletr  9751  xrre  9764  xaddge0  9822  xle2add  9823  xlt2add  9824  divelunit  9946  fzass4  10005  fzocatel  10142  exbtwnzlemex  10193  rebtwn2z  10198  qbtwnre  10200  modqid  10292  modqcyc  10302  modqaddabs  10305  modqaddmod  10306  mulqaddmodid  10307  modqadd2mod  10317  modqltm1p1mod  10319  modqsubmod  10325  modqsubmodmod  10326  modqmulmod  10332  modqmulmodr  10333  modqaddmulmod  10334  modqsubdir  10336  frec2uzisod  10350  iseqovex  10399  seqvalcd  10402  seqf  10404  seqovcd  10406  seq3fveq2  10412  seq3shft2  10416  monoord  10419  seq3split  10422  iseqf1olemnab  10431  seq3id2  10452  seq3distr  10456  expcl2lemap  10475  expnegzap  10497  ltexp2a  10515  le2sq2  10538  nn0ltexp2  10631  nn0opth2  10645  bcval5  10684  hashcl  10702  hashen  10705  fihashdom  10725  hashunlem  10726  hashun  10727  fimaxq  10749  zfz1isolem1  10762  zfz1iso  10763  cvg1nlemres  10936  cvg1n  10937  recvguniq  10946  resqrexlemp1rp  10957  resqrexlemoverl  10972  resqrexlemglsq  10973  resqrexlemex  10976  sqrtmul  10986  sqrtsq  10995  absexpzap  11031  absle  11040  abs3lem  11062  amgm2  11069  maxleastlt  11166  maxltsup  11169  fimaxre2  11177  xrmaxleastlt  11206  xrmaxltsup  11208  xrmaxaddlem  11210  climcn2  11259  addcn2  11260  mulcn2  11262  reccn2ap  11263  climcau  11297  summodclem2  11332  summodc  11333  fsumf1o  11340  fisumss  11342  fsum3cvg3  11346  fsumcl2lem  11348  fsumadd  11356  fsum2dlemstep  11384  mptfzshft  11392  fsumrev  11393  fsummulc2  11398  modfsummod  11408  fsumrelem  11421  binom  11434  cvgratnn  11481  mertenslemub  11484  prodmodc  11528  zproddc  11529  fprodf1o  11538  fprodssdc  11540  fprodmul  11541  fprodrev  11569  fprod2dlemstep  11572  efcllem  11609  tanaddaplem  11688  dvdsval2  11739  moddvds  11748  dvdsabseq  11794  dvdsflip  11798  oexpneg  11823  fldivndvdslt  11881  zsupcllemstep  11887  zssinfcl  11890  suprzubdc  11894  zsupssdc  11896  suprzcl2dc  11897  bezoutlemnewy  11938  bezoutlemstep  11939  bezoutlemeu  11949  dfgcd3  11952  bezout  11953  dvdsmulgcd  11967  bezoutr  11974  ialgrlem1st  11983  lcmgcdlem  12018  coprmdvds2  12034  qredeu  12038  rpdvds  12040  isprm5lem  12082  isprm6  12088  pw2dvdslemn  12106  nonsq  12148  crth  12165  eulerthlemh  12172  pclemdc  12229  pcprendvds2  12232  pceu  12236  pcval  12237  pczpre  12238  pcmul  12242  pcqmul  12244  pcqcl  12247  pcid  12264  pcneg  12265  pcgcd1  12268  pc2dvds  12270  pcprmpw2  12273  difsqpwdvds  12278  pcmpt  12282  pockthg  12296  1arith  12306  mul4sq  12333  ennnfonelemg  12345  ennnfonelemex  12356  ennnfonelemrnh  12358  ennnfonelemrn  12361  ennnfonelemdm  12362  ennnfonelemnn0  12364  ennnfonelemim  12366  ennnfone  12367  ctinfomlemom  12369  ctinf  12372  ctiunctlemfo  12381  nninfdclemcl  12390  nninfdclemf  12391  nninfdclemp1  12392  unbendc  12396  isstruct2r  12414  setscom  12443  opifismgmdc  12612  grprinvlem  12626  grpridd  12628  mndpropd  12663  mhmf1o  12680  0mhm  12691  mhmco  12692  mhmima  12693  mhmeql  12694  grppropd  12711  epttop  12843  topssnei  12915  restbasg  12921  restopnb  12934  cnfval  12947  cnpfval  12948  iscnp4  12971  cnpnei  12972  cnptopco  12975  cncnp  12983  cnrest2  12989  cnptoprest  12992  cnptoprest2  12993  lmss  12999  lmtopcnp  13003  neitx  13021  txcnp  13024  txrest  13029  txdis  13030  txlm  13032  cnmpt21  13044  imasnopn  13052  xmetres2  13132  blvalps  13141  blval  13142  bl2in  13156  blhalf  13161  blssps  13180  blss  13181  blssexps  13182  blssex  13183  ssblex  13184  blin2  13185  metss2lem  13250  bdmetval  13253  bdmopn  13257  metrest  13259  xmetxp  13260  xmetxpbl  13261  xmettx  13263  metcnp3  13264  txmetcnp  13271  addcncntoplem  13304  elcncf2  13314  mulc1cncf  13329  cncfco  13331  cncfmet  13332  mulcncf  13344  dedekindeulemub  13349  dedekindeulemloc  13350  dedekindeulemlu  13352  dedekindeu  13354  suplociccex  13356  dedekindicclemub  13358  dedekindicclemloc  13359  dedekindicclemlu  13361  dedekindicc  13364  ivthinclemlopn  13367  ivthinclemuopn  13369  ivthdec  13375  limcimolemlt  13386  limcimo  13387  cnplimccntop  13392  limccnp2lem  13398  limccnp2cntop  13399  dvfvalap  13403  dveflem  13440  reeff1olem  13445  reeff1oleme  13446  eflt  13449  sin0pilem2  13456  pilem3  13457  ptolemy  13498  ioocosf1o  13528  cxplt  13589  cxple  13590  cxplt3  13593  apcxp2  13611  rprelogbmul  13626  rprelogbdiv  13628  logbgt0b  13637  logbgcd1irrap  13641  lgsdir2lem5  13686  lgsdir  13689  lgsdi  13691  lgsne0  13692  2sqlem6  13709  2sqlem10  13714  nnti  13987  pwtrufal  13990  pwf1oexmid  13992  sssneq  13995  qdencn  14019  cvgcmp2n  14025  trilpolemlt1  14033  trirec0  14036  trirec0xor  14037  redc0  14049  reap0  14050  nconstwlpolemgt0  14055  supfz  14060  inffz  14061