Theorem simprl 520

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 481	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  1046  simp2rl  1050  simp3rl  1054  rmob  2996  disjiun  3919  reg3exmidlemwe  4488  0xp  4614  imainss  4949  fvmptt  5505  fcof1o  5683  isotr  5710  riota5f  5747  ovmpodf  5895  grprinvlem  5958  grpridd  5960  unielxp  6065  fnmpoovd  6105  1stconst  6111  2ndconst  6112  cnvf1olem  6114  tfrlemi14d  6223  tfrexlem  6224  tfr1onlemres  6239  tfrcllemres  6252  tfrcldm  6253  frecabcl  6289  nnaordi  6397  swoer  6450  qliftfun  6504  ecopovsymg  6521  th3qlem1  6524  mapen  6733  mapxpen  6735  fidifsnen  6757  fisbth  6770  findcard2d  6778  findcard2sd  6779  diffisn  6780  diffifi  6781  ac6sfi  6785  fimax2gtri  6788  fientri3  6796  nnwetri  6797  unsnfi  6800  unsnfidcex  6801  unsnfidcel  6802  fisseneq  6813  fidcenumlemrk  6835  fidcenumlemr  6836  isbth  6848  ordiso2  6913  difinfsnlem  6977  difinfinf  6979  ctmlemr  6986  ctssdccl  6989  fodjum  7011  fodju0  7012  exmidfodomrlemrALT  7052  dfplpq2  7155  dfmpq2  7156  mulpipqqs  7174  distrnqg  7188  ltexnqq  7209  subhalfnqq  7215  distrnq0  7260  prarloclemup  7296  prarloclem3  7298  prarloc  7304  genplt2i  7311  nqprl  7352  nqpru  7353  prmuloc  7367  mullocpr  7372  distrlem4prl  7385  distrlem4pru  7386  ltaddpr  7398  ltexprlemopl  7402  ltexprlemlol  7403  ltexprlemopu  7404  ltexprlemupu  7405  ltexprlemrl  7411  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  ltaprlem  7419  ltaprg  7420  prplnqu  7421  addextpr  7422  recexprlemdisj  7431  recexprlemloc  7432  recexprlem1ssl  7434  aptiprleml  7440  aptiprlemu  7441  ltmprr  7443  archpr  7444  cauappcvgprlemopl  7447  cauappcvgprlemopu  7449  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlem1  7460  cauappcvgprlem2  7461  cauappcvgprlemlim  7462  caucvgprlemnkj  7467  caucvgprlemopl  7470  caucvgprlemopu  7472  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprlem2  7481  caucvgprprlemnkltj  7490  caucvgprprlemnkeqj  7491  caucvgprprlemnjltk  7492  caucvgprprlemmu  7496  caucvgprprlemopl  7498  caucvgprprlemopu  7500  caucvgprprlemdisj  7503  caucvgprprlemloc  7504  caucvgprprlemexbt  7507  caucvgprprlemaddq  7509  caucvgprprlem2  7511  suplocexprlemrl  7518  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemex  7523  suplocexprlemub  7524  suplocexprlemlub  7525  recexgt0sr  7574  mulgt0sr  7579  prsrriota  7589  caucvgsrlemoffres  7601  suplocsrlem  7609  cnm  7633  addcnsr  7635  mulcnsr  7636  mulcnsrec  7644  axaddcl  7665  axmulcl  7667  axmulcom  7672  rereceu  7690  recriota  7691  axcaucvglemres  7700  axpre-suploclemres  7702  lelttr  7845  ltletr  7846  readdcan  7895  addcan  7935  addcan2  7936  addsub4  7998  ltadd2  8174  le2add  8199  lt2add  8200  lt2sub  8215  le2sub  8216  eqord1  8238  rimul  8340  rereim  8341  ltmul1  8347  apreim  8358  mulreim  8359  apcotr  8362  apadd1  8363  addext  8365  apneg  8366  mulext1  8367  mulext  8369  ltleap  8387  aprcl  8401  mulap0  8408  mulcanapd  8415  receuap  8423  rec11ap  8463  rec11rap  8464  divdivdivap  8466  ddcanap  8479  divadddivap  8480  conjmulap  8482  subrecap  8591  prodgt0gt0  8602  prodge0  8605  ltmul12a  8611  lemulge11  8617  lt2mul2div  8630  ltrec  8634  lerec  8635  lt2msq  8637  lerec2  8640  le2msq  8652  msq11  8653  ledivp1  8654  mulle0r  8695  suprzclex  9142  peano5uzti  9152  supinfneg  9383  infsupneg  9384  qapne  9424  xrlelttr  9582  xrltletr  9583  xrre  9596  xaddge0  9654  xle2add  9655  xlt2add  9656  divelunit  9778  fzass4  9835  fzocatel  9969  exbtwnzlemex  10020  rebtwn2z  10025  qbtwnre  10027  modqid  10115  modqcyc  10125  modqaddabs  10128  modqaddmod  10129  mulqaddmodid  10130  modqadd2mod  10140  modqltm1p1mod  10142  modqsubmod  10148  modqsubmodmod  10149  modqmulmod  10155  modqmulmodr  10156  modqaddmulmod  10157  modqsubdir  10159  frec2uzisod  10173  iseqovex  10222  seqvalcd  10225  seqf  10227  seqovcd  10229  seq3fveq2  10235  seq3shft2  10239  monoord  10242  seq3split  10245  iseqf1olemnab  10254  seq3id2  10275  seq3distr  10279  expcl2lemap  10298  expnegzap  10320  ltexp2a  10338  le2sq2  10361  nn0opth2  10463  bcval5  10502  hashcl  10520  hashen  10523  fihashdom  10542  hashunlem  10543  hashun  10544  fimaxq  10566  zfz1isolem1  10576  zfz1iso  10577  cvg1nlemres  10750  cvg1n  10751  recvguniq  10760  resqrexlemp1rp  10771  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemex  10790  sqrtmul  10800  sqrtsq  10809  absexpzap  10845  absle  10854  abs3lem  10876  amgm2  10883  maxleastlt  10980  maxltsup  10983  fimaxre2  10991  xrmaxleastlt  11018  xrmaxltsup  11020  xrmaxaddlem  11022  climcn2  11071  addcn2  11072  mulcn2  11074  reccn2ap  11075  climcau  11109  summodclem2  11144  summodc  11145  fsumf1o  11152  fisumss  11154  fsum3cvg3  11158  fsumcl2lem  11160  fsumadd  11168  fsum2dlemstep  11196  mptfzshft  11204  fsumrev  11205  fsummulc2  11210  modfsummod  11220  fsumrelem  11233  binom  11246  cvgratnn  11293  mertenslemub  11296  efcllem  11354  tanaddaplem  11434  dvdsval2  11485  moddvds  11491  dvdsabseq  11534  dvdsflip  11538  oexpneg  11563  fldivndvdslt  11621  zsupcllemstep  11627  zssinfcl  11630  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemeu  11684  dfgcd3  11687  bezout  11688  dvdsmulgcd  11702  bezoutr  11709  ialgrlem1st  11712  lcmgcdlem  11747  coprmdvds2  11763  qredeu  11767  rpdvds  11769  isprm6  11814  pw2dvdslemn  11832  nonsq  11874  crth  11889  ennnfonelemg  11905  ennnfonelemex  11916  ennnfonelemrnh  11918  ennnfonelemrn  11921  ennnfonelemdm  11922  ennnfonelemnn0  11924  ennnfonelemim  11926  ennnfone  11927  ctinfomlemom  11929  ctinf  11932  ctiunctlemfo  11941  isstruct2r  11959  setscom  11988  epttop  12248  topssnei  12320  restbasg  12326  restopnb  12339  cnfval  12352  cnpfval  12353  iscnp4  12376  cnpnei  12377  cnptopco  12380  cncnp  12388  cnrest2  12394  cnptoprest  12397  cnptoprest2  12398  lmss  12404  lmtopcnp  12408  neitx  12426  txcnp  12429  txrest  12434  txdis  12435  txlm  12437  cnmpt21  12449  imasnopn  12457  xmetres2  12537  blvalps  12546  blval  12547  bl2in  12561  blhalf  12566  blssps  12585  blss  12586  blssexps  12587  blssex  12588  ssblex  12589  blin2  12590  metss2lem  12655  bdmetval  12658  bdmopn  12662  metrest  12664  xmetxp  12665  xmetxpbl  12666  xmettx  12668  metcnp3  12669  txmetcnp  12676  addcncntoplem  12709  elcncf2  12719  mulc1cncf  12734  cncfco  12736  cncfmet  12737  mulcncf  12749  dedekindeulemub  12754  dedekindeulemloc  12755  dedekindeulemlu  12757  dedekindeu  12759  suplociccex  12761  dedekindicclemub  12763  dedekindicclemloc  12764  dedekindicclemlu  12766  dedekindicc  12769  ivthinclemlopn  12772  ivthinclemuopn  12774  ivthdec  12780  limcimolemlt  12791  limcimo  12792  cnplimccntop  12797  limccnp2lem  12803  limccnp2cntop  12804  dvfvalap  12808  dveflem  12844  sin0pilem2  12852  pilem3  12853  ptolemy  12894  nnti  13180  pwtrufal  13181  pwf1oexmid  13183  qdencn  13211  cvgcmp2n  13217  trilpolemlt1  13223  supfz  13226  inffz  13227