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  1052  simp2rl  1056  simp3rl  1060  rmob  3042  disjiun  3976  reg3exmidlemwe  4555  0xp  4683  imainss  5018  fvmptt  5576  fcof1o  5756  isotr  5783  riota5f  5821  ovmpodf  5969  grprinvlem  6032  grpridd  6034  unielxp  6139  fnmpoovd  6179  1stconst  6185  2ndconst  6186  cnvf1olem  6188  tfrlemi14d  6297  tfrexlem  6298  tfr1onlemres  6313  tfrcllemres  6326  tfrcldm  6327  frecabcl  6363  nnaordi  6472  swoer  6525  qliftfun  6579  ecopovsymg  6596  th3qlem1  6599  mapen  6808  mapxpen  6810  fidifsnen  6832  fisbth  6845  findcard2d  6853  findcard2sd  6854  diffisn  6855  diffifi  6856  ac6sfi  6860  fimax2gtri  6863  fientri3  6876  nnwetri  6877  unsnfi  6880  unsnfidcex  6881  unsnfidcel  6882  fisseneq  6893  fidcenumlemrk  6915  fidcenumlemr  6916  isbth  6928  ordiso2  6996  difinfsnlem  7060  difinfinf  7062  ctmlemr  7069  ctssdccl  7072  fodjum  7106  fodju0  7107  omniwomnimkv  7127  exmidfodomrlemrALT  7155  cc1  7202  cc2lem  7203  cc3  7205  cc4f  7206  cc4n  7208  dfplpq2  7291  dfmpq2  7292  mulpipqqs  7310  distrnqg  7324  ltexnqq  7345  subhalfnqq  7351  distrnq0  7396  prarloclemup  7432  prarloclem3  7434  prarloc  7440  genplt2i  7447  nqprl  7488  nqpru  7489  prmuloc  7503  mullocpr  7508  distrlem4prl  7521  distrlem4pru  7522  ltaddpr  7534  ltexprlemopl  7538  ltexprlemlol  7539  ltexprlemopu  7540  ltexprlemupu  7541  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  ltaprlem  7555  ltaprg  7556  prplnqu  7557  addextpr  7558  recexprlemdisj  7567  recexprlemloc  7568  recexprlem1ssl  7570  aptiprleml  7576  aptiprlemu  7577  ltmprr  7579  archpr  7580  cauappcvgprlemopl  7583  cauappcvgprlemopu  7585  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlem1  7596  cauappcvgprlem2  7597  cauappcvgprlemlim  7598  caucvgprlemnkj  7603  caucvgprlemopl  7606  caucvgprlemopu  7608  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlem2  7617  caucvgprprlemnkltj  7626  caucvgprprlemnkeqj  7627  caucvgprprlemnjltk  7628  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemopu  7636  caucvgprprlemdisj  7639  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  caucvgprprlemaddq  7645  caucvgprprlem2  7647  suplocexprlemrl  7654  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemex  7659  suplocexprlemub  7660  suplocexprlemlub  7661  recexgt0sr  7710  mulgt0sr  7715  prsrriota  7725  caucvgsrlemoffres  7737  suplocsrlem  7745  cnm  7769  addcnsr  7771  mulcnsr  7772  mulcnsrec  7780  axaddcl  7801  axmulcl  7803  axmulcom  7808  rereceu  7826  recriota  7827  axcaucvglemres  7836  axpre-suploclemres  7838  lelttr  7983  ltletr  7984  readdcan  8034  addcan  8074  addcan2  8075  addsub4  8137  ltadd2  8313  le2add  8338  lt2add  8339  lt2sub  8354  le2sub  8355  eqord1  8377  rimul  8479  rereim  8480  ltmul1  8486  apreim  8497  mulreim  8498  apcotr  8501  apadd1  8502  addext  8504  apneg  8505  mulext1  8506  mulext  8508  ltleap  8526  aprcl  8540  mulap0  8547  mulcanapd  8554  receuap  8562  rec11ap  8602  rec11rap  8603  divdivdivap  8605  ddcanap  8618  divadddivap  8619  conjmulap  8621  subrecap  8731  prodgt0gt0  8742  prodge0  8745  ltmul12a  8751  lemulge11  8757  lt2mul2div  8770  ltrec  8774  lerec  8775  lt2msq  8777  lerec2  8780  le2msq  8792  msq11  8793  ledivp1  8794  mulle0r  8835  suprzclex  9285  peano5uzti  9295  supinfneg  9529  infsupneg  9530  qapne  9573  xrlelttr  9738  xrltletr  9739  xrre  9752  xaddge0  9810  xle2add  9811  xlt2add  9812  divelunit  9934  fzass4  9993  fzocatel  10130  exbtwnzlemex  10181  rebtwn2z  10186  qbtwnre  10188  modqid  10280  modqcyc  10290  modqaddabs  10293  modqaddmod  10294  mulqaddmodid  10295  modqadd2mod  10305  modqltm1p1mod  10307  modqsubmod  10313  modqsubmodmod  10314  modqmulmod  10320  modqmulmodr  10321  modqaddmulmod  10322  modqsubdir  10324  frec2uzisod  10338  iseqovex  10387  seqvalcd  10390  seqf  10392  seqovcd  10394  seq3fveq2  10400  seq3shft2  10404  monoord  10407  seq3split  10410  iseqf1olemnab  10419  seq3id2  10440  seq3distr  10444  expcl2lemap  10463  expnegzap  10485  ltexp2a  10503  le2sq2  10526  nn0ltexp2  10619  nn0opth2  10633  bcval5  10672  hashcl  10690  hashen  10693  fihashdom  10712  hashunlem  10713  hashun  10714  fimaxq  10736  zfz1isolem1  10749  zfz1iso  10750  cvg1nlemres  10923  cvg1n  10924  recvguniq  10933  resqrexlemp1rp  10944  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemex  10963  sqrtmul  10973  sqrtsq  10982  absexpzap  11018  absle  11027  abs3lem  11049  amgm2  11056  maxleastlt  11153  maxltsup  11156  fimaxre2  11164  xrmaxleastlt  11193  xrmaxltsup  11195  xrmaxaddlem  11197  climcn2  11246  addcn2  11247  mulcn2  11249  reccn2ap  11250  climcau  11284  summodclem2  11319  summodc  11320  fsumf1o  11327  fisumss  11329  fsum3cvg3  11333  fsumcl2lem  11335  fsumadd  11343  fsum2dlemstep  11371  mptfzshft  11379  fsumrev  11380  fsummulc2  11385  modfsummod  11395  fsumrelem  11408  binom  11421  cvgratnn  11468  mertenslemub  11471  prodmodc  11515  zproddc  11516  fprodf1o  11525  fprodssdc  11527  fprodmul  11528  fprodrev  11556  fprod2dlemstep  11559  efcllem  11596  tanaddaplem  11675  dvdsval2  11726  moddvds  11735  dvdsabseq  11781  dvdsflip  11785  oexpneg  11810  fldivndvdslt  11868  zsupcllemstep  11874  zssinfcl  11877  suprzubdc  11881  zsupssdc  11883  suprzcl2dc  11884  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemeu  11936  dfgcd3  11939  bezout  11940  dvdsmulgcd  11954  bezoutr  11961  ialgrlem1st  11970  lcmgcdlem  12005  coprmdvds2  12021  qredeu  12025  rpdvds  12027  isprm5lem  12069  isprm6  12075  pw2dvdslemn  12093  nonsq  12135  crth  12152  eulerthlemh  12159  pclemdc  12216  pcprendvds2  12219  pceu  12223  pcval  12224  pczpre  12225  pcmul  12229  pcqmul  12231  pcqcl  12234  pcid  12251  pcneg  12252  pcgcd1  12255  pc2dvds  12257  pcprmpw2  12260  difsqpwdvds  12265  pcmpt  12269  pockthg  12283  1arith  12293  mul4sq  12320  ennnfonelemg  12332  ennnfonelemex  12343  ennnfonelemrnh  12345  ennnfonelemrn  12348  ennnfonelemdm  12349  ennnfonelemnn0  12351  ennnfonelemim  12353  ennnfone  12354  ctinfomlemom  12356  ctinf  12359  ctiunctlemfo  12368  nninfdclemcl  12377  nninfdclemf  12378  nninfdclemp1  12379  unbendc  12383  isstruct2r  12401  setscom  12430  epttop  12690  topssnei  12762  restbasg  12768  restopnb  12781  cnfval  12794  cnpfval  12795  iscnp4  12818  cnpnei  12819  cnptopco  12822  cncnp  12830  cnrest2  12836  cnptoprest  12839  cnptoprest2  12840  lmss  12846  lmtopcnp  12850  neitx  12868  txcnp  12871  txrest  12876  txdis  12877  txlm  12879  cnmpt21  12891  imasnopn  12899  xmetres2  12979  blvalps  12988  blval  12989  bl2in  13003  blhalf  13008  blssps  13027  blss  13028  blssexps  13029  blssex  13030  ssblex  13031  blin2  13032  metss2lem  13097  bdmetval  13100  bdmopn  13104  metrest  13106  xmetxp  13107  xmetxpbl  13108  xmettx  13110  metcnp3  13111  txmetcnp  13118  addcncntoplem  13151  elcncf2  13161  mulc1cncf  13176  cncfco  13178  cncfmet  13179  mulcncf  13191  dedekindeulemub  13196  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeu  13201  suplociccex  13203  dedekindicclemub  13205  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthdec  13222  limcimolemlt  13233  limcimo  13234  cnplimccntop  13239  limccnp2lem  13245  limccnp2cntop  13246  dvfvalap  13250  dveflem  13287  reeff1olem  13292  reeff1oleme  13293  eflt  13296  sin0pilem2  13303  pilem3  13304  ptolemy  13345  ioocosf1o  13375  cxplt  13436  cxple  13437  cxplt3  13440  apcxp2  13458  rprelogbmul  13473  rprelogbdiv  13475  logbgt0b  13484  logbgcd1irrap  13488  lgsdir2lem5  13533  lgsdir  13536  lgsdi  13538  lgsne0  13539  2sqlem6  13556  2sqlem10  13561  nnti  13834  pwtrufal  13837  pwf1oexmid  13839  sssneq  13842  qdencn  13866  cvgcmp2n  13872  trilpolemlt1  13880  trirec0  13883  trirec0xor  13884  redc0  13896  reap0  13897  nconstwlpolemgt0  13902  supfz  13907  inffz  13908