Theorem simprl 499

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1rl  1011  simp2rl  1015  simp3rl  1019  rmob  2945  disjiun  3862  reg3exmidlemwe  4422  0xp  4547  imainss  4880  fvmptt  5430  fcof1o  5606  isotr  5633  riota5f  5670  ovmpt2df  5814  grprinvlem  5877  grpridd  5879  unielxp  5982  1stconst  6024  2ndconst  6025  cnvf1olem  6027  tfrlemi14d  6136  tfrexlem  6137  tfr1onlemres  6152  tfrcllemres  6165  tfrcldm  6166  frecabcl  6202  nnaordi  6307  swoer  6360  qliftfun  6414  ecopovsymg  6431  th3qlem1  6434  mapen  6642  mapxpen  6644  fidifsnen  6666  fisbth  6679  findcard2d  6687  findcard2sd  6688  diffisn  6689  diffifi  6690  ac6sfi  6694  fimax2gtri  6697  fientri3  6705  nnwetri  6706  unsnfi  6709  unsnfidcex  6710  unsnfidcel  6711  fisseneq  6722  fidcenumlemrk  6743  fidcenumlemr  6744  isbth  6756  ordiso2  6808  ctmlemr  6870  fodjum  6889  fodju0  6890  exmidfodomrlemrALT  6926  dfplpq2  7010  dfmpq2  7011  mulpipqqs  7029  distrnqg  7043  ltexnqq  7064  subhalfnqq  7070  distrnq0  7115  prarloclemup  7151  prarloclem3  7153  prarloc  7159  genplt2i  7166  nqprl  7207  nqpru  7208  prmuloc  7222  mullocpr  7227  distrlem4prl  7240  distrlem4pru  7241  ltaddpr  7253  ltexprlemopl  7257  ltexprlemlol  7258  ltexprlemopu  7259  ltexprlemupu  7260  ltexprlemrl  7266  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  ltaprlem  7274  ltaprg  7275  prplnqu  7276  addextpr  7277  recexprlemdisj  7286  recexprlemloc  7287  recexprlem1ssl  7289  aptiprleml  7295  aptiprlemu  7296  ltmprr  7298  archpr  7299  cauappcvgprlemopl  7302  cauappcvgprlemopu  7304  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlem1  7315  cauappcvgprlem2  7316  cauappcvgprlemlim  7317  caucvgprlemnkj  7322  caucvgprlemopl  7325  caucvgprlemopu  7327  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlem2  7336  caucvgprprlemnkltj  7345  caucvgprprlemnkeqj  7346  caucvgprprlemnjltk  7347  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemopu  7355  caucvgprprlemdisj  7358  caucvgprprlemloc  7359  caucvgprprlemexbt  7362  caucvgprprlemaddq  7364  caucvgprprlem2  7366  recexgt0sr  7416  mulgt0sr  7420  prsrriota  7430  caucvgsrlemoffres  7442  addcnsr  7468  mulcnsr  7469  mulcnsrec  7477  axaddcl  7498  axmulcl  7500  axmulcom  7503  rereceu  7521  recriota  7522  axcaucvglemres  7531  lelttr  7670  ltletr  7671  readdcan  7719  addcan  7759  addcan2  7760  addsub4  7822  ltadd2  7994  le2add  8019  lt2add  8020  lt2sub  8035  le2sub  8036  eqord1  8058  rimul  8159  rereim  8160  ltmul1  8166  apreim  8177  mulreim  8178  apcotr  8181  apadd1  8182  addext  8184  apneg  8185  mulext1  8186  mulext  8188  ltleap  8204  mulap0  8220  mulcanapd  8227  receuap  8235  rec11ap  8274  rec11rap  8275  divdivdivap  8277  ddcanap  8290  divadddivap  8291  conjmulap  8293  prodgt0gt0  8409  prodge0  8412  ltmul12a  8418  lemulge11  8424  lt2mul2div  8437  ltrec  8441  lerec  8442  lt2msq  8444  lerec2  8447  le2msq  8459  msq11  8460  ledivp1  8461  mulle0r  8502  suprzclex  8943  peano5uzti  8953  supinfneg  9182  infsupneg  9183  qapne  9223  xrlelttr  9372  xrltletr  9373  xrre  9386  xaddge0  9444  xle2add  9445  xlt2add  9446  divelunit  9568  fzass4  9625  fzocatel  9759  exbtwnzlemex  9810  rebtwn2z  9815  qbtwnre  9817  modqid  9905  modqcyc  9915  modqaddabs  9918  modqaddmod  9919  mulqaddmodid  9920  modqadd2mod  9930  modqltm1p1mod  9932  modqsubmod  9938  modqsubmodmod  9939  modqmulmod  9945  modqmulmodr  9946  modqaddmulmod  9947  modqsubdir  9949  frec2uzisod  9963  iseqovex  10016  iseqval  10017  iseqfclt  10025  seqf  10026  seq3fveq2  10034  seq3shft2  10038  monoord  10042  seq3split  10045  iseqf1olemnab  10054  seq3id2  10075  seq3distr  10079  expcl2lemap  10098  expnegzap  10120  ltexp2a  10138  le2sq2  10161  nn0opth2  10263  bcval5  10302  hashcl  10320  hashen  10323  fihashdom  10342  hashunlem  10343  hashun  10344  fimaxq  10366  zfz1isolem1  10376  zfz1iso  10377  cvg1nlemres  10549  cvg1n  10550  recvguniq  10559  resqrexlemp1rp  10570  resqrexlemoverl  10585  resqrexlemglsq  10586  resqrexlemex  10589  sqrtmul  10599  sqrtsq  10608  absexpzap  10644  absle  10653  abs3lem  10675  amgm2  10682  maxleastlt  10779  maxltsup  10782  fimaxre2  10789  xrmaxleastlt  10815  xrmaxltsup  10817  xrmaxaddlem  10819  climcn2  10868  addcn2  10869  mulcn2  10871  reccn2ap  10872  climcau  10906  summodclem2  10941  summodc  10942  fsumf1o  10949  fisumss  10951  fsum3cvg3  10955  fsumcl2lem  10957  fsumadd  10965  fsum2dlemstep  10993  mptfzshft  11001  fsumrev  11002  fsummulc2  11007  modfsummod  11017  fsumrelem  11030  binom  11043  cvgratnn  11090  mertenslemub  11093  efcllem  11114  tanaddaplem  11194  dvdsval2  11242  moddvds  11248  dvdsabseq  11291  dvdsflip  11295  oexpneg  11320  fldivndvdslt  11378  zsupcllemstep  11384  zssinfcl  11387  bezoutlemnewy  11428  bezoutlemstep  11429  bezoutlemeu  11439  dfgcd3  11442  bezout  11443  dvdsmulgcd  11457  bezoutr  11464  ialgrlem1st  11467  lcmgcdlem  11502  coprmdvds2  11518  qredeu  11522  rpdvds  11524  isprm6  11569  pw2dvdslemn  11586  nonsq  11628  crth  11643  isstruct2r  11670  setscom  11699  epttop  11958  topssnei  12030  restbasg  12036  restopnb  12049  cnfval  12062  cnpfval  12063  iscnp4  12085  cnpnei  12086  cnptopco  12089  cncnp  12097  cnrest2  12103  cnptoprest  12106  cnptoprest2  12107  lmss  12113  lmtopcnp  12117  xmetres2  12181  blvalps  12190  blval  12191  bl2in  12205  blhalf  12210  blssps  12229  blss  12230  blssexps  12231  blssex  12232  ssblex  12233  blin2  12234  metss2lem  12299  bdmetval  12302  bdmopn  12306  metrest  12308  metcnp3  12309  elcncf2  12343  mulc1cncf  12358  cncfco  12360  cncfmet  12361  mulcncf  12370  nnti  12613  qdencn  12636  supfz  12637  inffz  12638