Theorem simprl 529

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  dfifp2dc  987  simp1rl  1086  simp2rl  1090  simp3rl  1094  rmob  3122  elpr2elpr  3854  disjiun  4078  reg3exmidlemwe  4671  0xp  4799  imainss  5144  iotam  5310  fvmptt  5728  fcof1o  5919  isotr  5946  riota5f  5987  ovmpodf  6142  unielxp  6326  fnmpoovd  6367  1stconst  6373  2ndconst  6374  cnvf1olem  6376  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemres  6501  tfrcllemres  6514  tfrcldm  6515  frecabcl  6551  nnaordi  6662  swoer  6716  qliftfun  6772  ecopovsymg  6789  th3qlem1  6792  pw2f1odclem  7003  mapen  7015  mapxpen  7017  fidifsnen  7040  fisbth  7053  findcard2d  7061  findcard2sd  7062  diffisn  7063  diffifi  7064  ac6sfi  7068  fidcen  7069  fimax2gtri  7072  fientri3  7088  nnwetri  7089  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  fisseneq  7107  fidcenumlemrk  7132  fidcenumlemr  7133  isbth  7145  ordiso2  7213  difinfsnlem  7277  difinfinf  7279  ctmlemr  7286  ctssdccl  7289  fodjum  7324  fodju0  7325  omniwomnimkv  7345  exmidfodomrlemrALT  7392  netap  7451  exmidmotap  7458  cc1  7462  cc2lem  7463  cc3  7465  cc4f  7466  cc4n  7468  dfplpq2  7552  dfmpq2  7553  mulpipqqs  7571  distrnqg  7585  ltexnqq  7606  subhalfnqq  7612  distrnq0  7657  prarloclemup  7693  prarloclem3  7695  prarloc  7701  genplt2i  7708  nqprl  7749  nqpru  7750  prmuloc  7764  mullocpr  7769  distrlem4prl  7782  distrlem4pru  7783  ltaddpr  7795  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  ltaprlem  7816  ltaprg  7817  prplnqu  7818  addextpr  7819  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssl  7831  aptiprleml  7837  aptiprlemu  7838  ltmprr  7840  archpr  7841  cauappcvgprlemopl  7844  cauappcvgprlemopu  7846  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgprlemlim  7859  caucvgprlemnkj  7864  caucvgprlemopl  7867  caucvgprlemopu  7869  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlem2  7878  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnjltk  7889  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemdisj  7900  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  caucvgprprlemaddq  7906  caucvgprprlem2  7908  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  suplocexprlemlub  7922  recexgt0sr  7971  mulgt0sr  7976  prsrriota  7986  caucvgsrlemoffres  7998  suplocsrlem  8006  cnm  8030  addcnsr  8032  mulcnsr  8033  mulcnsrec  8041  axaddcl  8062  axmulcl  8064  axmulcom  8069  rereceu  8087  recriota  8088  axcaucvglemres  8097  axpre-suploclemres  8099  lelttr  8246  ltletr  8247  readdcan  8297  addcan  8337  addcan2  8338  addsub4  8400  ltadd2  8577  le2add  8602  lt2add  8603  lt2sub  8618  le2sub  8619  eqord1  8641  rimul  8743  rereim  8744  ltmul1  8750  apreim  8761  mulreim  8762  apcotr  8765  apadd1  8766  addext  8768  apneg  8769  mulext1  8770  mulext  8772  ltleap  8790  aprcl  8804  mulap0  8812  mulcanapd  8819  receuap  8827  recapb  8829  rec11ap  8868  rec11rap  8869  divdivdivap  8871  ddcanap  8884  divadddivap  8885  conjmulap  8887  subrecap  8997  prodgt0gt0  9009  prodge0  9012  ltmul12a  9018  lemulge11  9024  lt2mul2div  9037  ltrec  9041  lerec  9042  lt2msq  9044  lerec2  9047  le2msq  9059  msq11  9060  ledivp1  9061  mulle0r  9102  suprzclex  9556  peano5uzti  9566  supinfneg  9802  infsupneg  9803  qapne  9846  xrlelttr  10014  xrltletr  10015  xrre  10028  xaddge0  10086  xle2add  10087  xlt2add  10088  divelunit  10210  fzass4  10270  fzocatel  10417  zsupcllemstep  10461  zssinfcl  10464  suprzubdc  10468  zsupssdc  10470  suprzcl2dc  10471  exbtwnzlemex  10481  rebtwn2z  10486  qbtwnre  10488  modqid  10583  modqcyc  10593  modqaddabs  10596  modqaddmod  10597  mulqaddmodid  10598  modqadd2mod  10608  modqltm1p1mod  10610  modqsubmod  10616  modqsubmodmod  10617  modqmulmod  10623  modqmulmodr  10624  modqaddmulmod  10625  modqsubdir  10627  frec2uzisod  10641  iseqovex  10692  seqvalcd  10695  seq1g  10697  seqf  10698  seqovcd  10701  seqm1g  10708  seq3fveq2  10709  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  iseqf1olemnab  10735  seqf1oglem1  10753  seqf1og  10755  seq3id2  10760  seqhomog  10764  seq3distr  10766  expcl2lemap  10785  expnegzap  10807  ltexp2a  10825  le2sq2  10849  nn0ltexp2  10943  nn0opth2  10958  bcval5  10997  hashcl  11015  hashen  11018  fihashdom  11037  hashunlem  11038  hashun  11039  fimaxq  11062  zfz1isolem1  11075  zfz1iso  11076  lencl  11088  sswrd  11093  fstwrdne0  11124  lswlgt0cl  11137  swrdval  11195  wrdind  11269  wrd2ind  11270  swrdccatfn  11271  swrdccatin1  11272  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12  11280  pfxccat3a  11285  reuccatpfxs1  11294  cvg1nlemres  11511  cvg1n  11512  recvguniq  11521  resqrexlemp1rp  11532  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemex  11551  sqrtmul  11561  sqrtsq  11570  absexpzap  11606  absle  11615  abs3lem  11637  amgm2  11644  maxleastlt  11741  maxltsup  11744  fimaxre2  11753  xrmaxleastlt  11782  xrmaxltsup  11784  xrmaxaddlem  11786  climcn2  11835  addcn2  11836  mulcn2  11838  reccn2ap  11839  climcau  11873  summodclem2  11908  summodc  11909  fsumf1o  11916  fisumss  11918  fsum3cvg3  11922  fsumcl2lem  11924  fsumadd  11932  fsum2dlemstep  11960  mptfzshft  11968  fsumrev  11969  fsummulc2  11974  modfsummod  11984  fsumrelem  11997  binom  12010  cvgratnn  12057  mertenslemub  12060  prodmodc  12104  zproddc  12105  fprodf1o  12114  fprodssdc  12116  fprodmul  12117  fprodrev  12145  fprod2dlemstep  12148  efcllem  12185  tanaddaplem  12264  dvdsval2  12316  moddvds  12325  dvdsabseq  12373  dvdsflip  12377  oexpneg  12403  fldivndvdslt  12463  bitsfi  12483  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemeu  12543  dfgcd3  12546  bezout  12547  dvdsmulgcd  12561  bezoutr  12568  nninfctlemfo  12576  ialgrlem1st  12579  lcmgcdlem  12614  coprmdvds2  12630  qredeu  12634  rpdvds  12636  isprm5lem  12678  isprm6  12684  pw2dvdslemn  12702  nonsq  12744  crth  12761  eulerthlemh  12768  pclemdc  12826  pcprendvds2  12829  pceu  12833  pcval  12834  pczpre  12835  pcmul  12839  pcqmul  12841  pcqcl  12844  pcid  12862  pcneg  12863  pcgcd1  12866  pc2dvds  12868  pcprmpw2  12871  difsqpwdvds  12876  pcmpt  12881  pockthg  12895  1arith  12905  mul4sq  12932  4sqexercise2  12937  ennnfonelemg  12989  ennnfonelemex  13000  ennnfonelemrnh  13002  ennnfonelemrn  13005  ennnfonelemdm  13006  ennnfonelemnn0  13008  ennnfonelemim  13010  ennnfone  13011  ctinfomlemom  13013  ctinf  13016  ctiunctlemfo  13025  nninfdclemcl  13034  nninfdclemf  13035  nninfdclemp1  13036  unbendc  13040  isstruct2r  13058  setscom  13087  qusval  13371  ercpbl  13379  opifismgmdc  13419  grpinvalem  13433  grprida  13435  igsumvalx  13437  gsumfzval  13439  gsumpropd2  13441  gsumval2  13445  sgrppropd  13461  prdssgrpd  13463  mndpropd  13488  issubmnd  13490  submnd0  13492  prdsmndd  13496  mhmf1o  13518  0mhm  13534  resmhm  13535  mhmco  13538  mhmima  13539  mhmeql  13540  gsumwsubmcl  13544  gsumfzcl  13547  grppropd  13565  grpinvid1  13600  grpinvid2  13601  grplcan  13610  grplmulf1o  13622  grpnpncan0  13644  dfgrp3mlem  13646  grplactcnv  13650  pwssub  13661  mulgval  13674  mulgfng  13676  mulg1  13681  mulgnnp1  13682  mulgneg  13692  mulgnndir  13703  mulgdirlem  13705  mulgnn0ass  13710  mulgass  13711  subgmulg  13740  issubg4m  13745  subgintm  13750  0nsg  13766  eqgcpbl  13780  ghmmulg  13808  ghmpreima  13818  ghmeql  13819  ghmnsgima  13820  ghmnsgpreima  13821  ghmf1  13825  ghmf1o  13827  conjghm  13828  conjnmzb  13832  qusghm  13834  ablpncan3  13869  invghm  13881  eqgabl  13882  qusecsub  13883  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  imasrng  13934  qusrng  13936  srglmhm  13971  srgrmhm  13972  ringpropd  14016  ringlghm  14039  ringrghm  14040  imasring  14042  qusring2  14044  opprrngbg  14056  dvdsrvald  14072  dvdsrd  14073  dvdsrex  14077  dvdsrtr  14080  unitgrp  14095  unitpropdg  14127  rhmopp  14155  isnzr2  14163  issubrng2  14189  subrngintm  14191  subrgintm  14222  rhmpropd  14233  aprap  14265  lmodprop2d  14327  rmodislmodlem  14329  lssvacl  14344  lssvsubcl  14345  lssvscl  14354  islss3  14358  lsspropdg  14410  rnglidlmcl  14459  2idlcpblrng  14502  crngridl  14509  expghmap  14586  mulgghm2  14587  mulgrhm  14588  znf1o  14630  znleval  14632  znidom  14636  psrval  14645  mplsubgfilemcl  14678  epttop  14779  topssnei  14851  restbasg  14857  restopnb  14870  cnfval  14883  cnpfval  14884  iscnp4  14907  cnpnei  14908  cnptopco  14911  cncnp  14919  cnrest2  14925  cnptoprest  14928  cnptoprest2  14929  lmss  14935  lmtopcnp  14939  neitx  14957  txcnp  14960  txrest  14965  txdis  14966  txlm  14968  cnmpt21  14980  imasnopn  14988  xmetres2  15068  blvalps  15077  blval  15078  bl2in  15092  blhalf  15097  blssps  15116  blss  15117  blssexps  15118  blssex  15119  ssblex  15120  blin2  15121  metss2lem  15186  bdmetval  15189  bdmopn  15193  metrest  15195  xmetxp  15196  xmetxpbl  15197  xmettx  15199  metcnp3  15200  txmetcnp  15207  addcncntoplem  15250  elcncf2  15263  mulc1cncf  15278  cncfco  15280  cncfmet  15281  mulcncf  15297  dedekindeulemub  15307  dedekindeulemloc  15308  dedekindeulemlu  15310  dedekindeu  15312  suplociccex  15314  dedekindicclemub  15316  dedekindicclemloc  15317  dedekindicclemlu  15319  dedekindicc  15322  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthdec  15333  ivthreinc  15334  dich0  15341  limcimolemlt  15353  limcimo  15354  cnplimccntop  15359  limccnp2lem  15365  limccnp2cntop  15366  dvfvalap  15370  dvmptfsum  15414  dveflem  15415  plyco  15448  plycn  15451  plyrecj  15452  reeff1olem  15460  reeff1oleme  15461  eflt  15464  sin0pilem2  15471  pilem3  15472  ptolemy  15513  ioocosf1o  15543  cxplt  15605  cxple  15606  cxplt3  15609  apcxp2  15628  rprelogbmul  15644  rprelogbdiv  15646  logbgt0b  15655  logbgcd1irrap  15659  fsumdvdsmul  15680  perfectlem2  15689  lgsdir2lem5  15726  lgsdir  15729  lgsdi  15731  lgsne0  15732  gausslemma2dlem1f1o  15754  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem2  15776  lgsquad2  15777  2sqlem6  15814  2sqlem10  15819  upgredg  15957  vtxedgfi  16048  vtxlpfi  16049  upgr2wlkdc  16116  clwwlkccatlem  16137  nnti  16415  pwtrufal  16422  pwf1oexmid  16424  sssneq  16427  qdencn  16455  cvgcmp2n  16461  trilpolemlt1  16469  trirec0  16472  trirec0xor  16473  redc0  16485  reap0  16486  cndcap  16487  nconstwlpolemgt0  16492  neap0mkv  16497  supfz  16499  inffz  16500