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:  simp1rl  1064  simp2rl  1068  simp3rl  1072  rmob  3079  disjiun  4025  reg3exmidlemwe  4612  0xp  4740  imainss  5082  iotam  5247  fvmptt  5650  fcof1o  5833  isotr  5860  riota5f  5899  ovmpodf  6051  unielxp  6229  fnmpoovd  6270  1stconst  6276  2ndconst  6277  cnvf1olem  6279  tfrlemi14d  6388  tfrexlem  6389  tfr1onlemres  6404  tfrcllemres  6417  tfrcldm  6418  frecabcl  6454  nnaordi  6563  swoer  6617  qliftfun  6673  ecopovsymg  6690  th3qlem1  6693  pw2f1odclem  6892  mapen  6904  mapxpen  6906  fidifsnen  6928  fisbth  6941  findcard2d  6949  findcard2sd  6950  diffisn  6951  diffifi  6952  ac6sfi  6956  fimax2gtri  6959  fientri3  6973  nnwetri  6974  unsnfi  6977  unsnfidcex  6978  unsnfidcel  6979  fisseneq  6990  fidcenumlemrk  7015  fidcenumlemr  7016  isbth  7028  ordiso2  7096  difinfsnlem  7160  difinfinf  7162  ctmlemr  7169  ctssdccl  7172  fodjum  7207  fodju0  7208  omniwomnimkv  7228  exmidfodomrlemrALT  7265  netap  7316  exmidmotap  7323  cc1  7327  cc2lem  7328  cc3  7330  cc4f  7331  cc4n  7333  dfplpq2  7416  dfmpq2  7417  mulpipqqs  7435  distrnqg  7449  ltexnqq  7470  subhalfnqq  7476  distrnq0  7521  prarloclemup  7557  prarloclem3  7559  prarloc  7565  genplt2i  7572  nqprl  7613  nqpru  7614  prmuloc  7628  mullocpr  7633  distrlem4prl  7646  distrlem4pru  7647  ltaddpr  7659  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  ltaprlem  7680  ltaprg  7681  prplnqu  7682  addextpr  7683  recexprlemdisj  7692  recexprlemloc  7693  recexprlem1ssl  7695  aptiprleml  7701  aptiprlemu  7702  ltmprr  7704  archpr  7705  cauappcvgprlemopl  7708  cauappcvgprlemopu  7710  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlem1  7721  cauappcvgprlem2  7722  cauappcvgprlemlim  7723  caucvgprlemnkj  7728  caucvgprlemopl  7731  caucvgprlemopu  7733  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlem2  7742  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemnjltk  7753  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemopu  7761  caucvgprprlemdisj  7764  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  caucvgprprlemaddq  7770  caucvgprprlem2  7772  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemex  7784  suplocexprlemub  7785  suplocexprlemlub  7786  recexgt0sr  7835  mulgt0sr  7840  prsrriota  7850  caucvgsrlemoffres  7862  suplocsrlem  7870  cnm  7894  addcnsr  7896  mulcnsr  7897  mulcnsrec  7905  axaddcl  7926  axmulcl  7928  axmulcom  7933  rereceu  7951  recriota  7952  axcaucvglemres  7961  axpre-suploclemres  7963  lelttr  8110  ltletr  8111  readdcan  8161  addcan  8201  addcan2  8202  addsub4  8264  ltadd2  8440  le2add  8465  lt2add  8466  lt2sub  8481  le2sub  8482  eqord1  8504  rimul  8606  rereim  8607  ltmul1  8613  apreim  8624  mulreim  8625  apcotr  8628  apadd1  8629  addext  8631  apneg  8632  mulext1  8633  mulext  8635  ltleap  8653  aprcl  8667  mulap0  8675  mulcanapd  8682  receuap  8690  recapb  8692  rec11ap  8731  rec11rap  8732  divdivdivap  8734  ddcanap  8747  divadddivap  8748  conjmulap  8750  subrecap  8860  prodgt0gt0  8872  prodge0  8875  ltmul12a  8881  lemulge11  8887  lt2mul2div  8900  ltrec  8904  lerec  8905  lt2msq  8907  lerec2  8910  le2msq  8922  msq11  8923  ledivp1  8924  mulle0r  8965  suprzclex  9418  peano5uzti  9428  supinfneg  9663  infsupneg  9664  qapne  9707  xrlelttr  9875  xrltletr  9876  xrre  9889  xaddge0  9947  xle2add  9948  xlt2add  9949  divelunit  10071  fzass4  10131  fzocatel  10269  exbtwnzlemex  10321  rebtwn2z  10326  qbtwnre  10328  modqid  10423  modqcyc  10433  modqaddabs  10436  modqaddmod  10437  mulqaddmodid  10438  modqadd2mod  10448  modqltm1p1mod  10450  modqsubmod  10456  modqsubmodmod  10457  modqmulmod  10463  modqmulmodr  10464  modqaddmulmod  10465  modqsubdir  10467  frec2uzisod  10481  iseqovex  10532  seqvalcd  10535  seq1g  10537  seqf  10538  seqovcd  10541  seqm1g  10548  seq3fveq2  10549  seq3shft2  10555  seqshft2g  10556  monoord  10559  seq3split  10562  seqsplitg  10563  iseqf1olemnab  10575  seqf1oglem1  10593  seqf1og  10595  seq3id2  10600  seqhomog  10604  seq3distr  10606  expcl2lemap  10625  expnegzap  10647  ltexp2a  10665  le2sq2  10689  nn0ltexp2  10783  nn0opth2  10798  bcval5  10837  hashcl  10855  hashen  10858  fihashdom  10877  hashunlem  10878  hashun  10879  fimaxq  10901  zfz1isolem1  10914  zfz1iso  10915  lencl  10921  sswrd  10926  fstwrdne0  10956  cvg1nlemres  11132  cvg1n  11133  recvguniq  11142  resqrexlemp1rp  11153  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemex  11172  sqrtmul  11182  sqrtsq  11191  absexpzap  11227  absle  11236  abs3lem  11258  amgm2  11265  maxleastlt  11362  maxltsup  11365  fimaxre2  11373  xrmaxleastlt  11402  xrmaxltsup  11404  xrmaxaddlem  11406  climcn2  11455  addcn2  11456  mulcn2  11458  reccn2ap  11459  climcau  11493  summodclem2  11528  summodc  11529  fsumf1o  11536  fisumss  11538  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  fsum2dlemstep  11580  mptfzshft  11588  fsumrev  11589  fsummulc2  11594  modfsummod  11604  fsumrelem  11617  binom  11630  cvgratnn  11677  mertenslemub  11680  prodmodc  11724  zproddc  11725  fprodf1o  11734  fprodssdc  11736  fprodmul  11737  fprodrev  11765  fprod2dlemstep  11768  efcllem  11805  tanaddaplem  11884  dvdsval2  11936  moddvds  11945  dvdsabseq  11992  dvdsflip  11996  oexpneg  12021  fldivndvdslt  12079  zsupcllemstep  12085  zssinfcl  12088  suprzubdc  12092  zsupssdc  12094  suprzcl2dc  12095  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemeu  12147  dfgcd3  12150  bezout  12151  dvdsmulgcd  12165  bezoutr  12172  nninfctlemfo  12180  ialgrlem1st  12183  lcmgcdlem  12218  coprmdvds2  12234  qredeu  12238  rpdvds  12240  isprm5lem  12282  isprm6  12288  pw2dvdslemn  12306  nonsq  12348  crth  12365  eulerthlemh  12372  pclemdc  12429  pcprendvds2  12432  pceu  12436  pcval  12437  pczpre  12438  pcmul  12442  pcqmul  12444  pcqcl  12447  pcid  12465  pcneg  12466  pcgcd1  12469  pc2dvds  12471  pcprmpw2  12474  difsqpwdvds  12479  pcmpt  12484  pockthg  12498  1arith  12508  mul4sq  12535  4sqexercise2  12540  ennnfonelemg  12563  ennnfonelemex  12574  ennnfonelemrnh  12576  ennnfonelemrn  12579  ennnfonelemdm  12580  ennnfonelemnn0  12582  ennnfonelemim  12584  ennnfone  12585  ctinfomlemom  12587  ctinf  12590  ctiunctlemfo  12599  nninfdclemcl  12608  nninfdclemf  12609  nninfdclemp1  12610  unbendc  12614  isstruct2r  12632  setscom  12661  qusval  12909  ercpbl  12917  opifismgmdc  12957  grpinvalem  12971  grprida  12973  igsumvalx  12975  gsumfzval  12977  gsumpropd2  12979  gsumval2  12983  sgrppropd  12999  mndpropd  13024  issubmnd  13026  submnd0  13028  mhmf1o  13045  0mhm  13061  resmhm  13062  mhmco  13065  mhmima  13066  mhmeql  13067  gsumwsubmcl  13071  gsumfzcl  13074  grppropd  13092  grpinvid1  13127  grpinvid2  13128  grplcan  13137  grplmulf1o  13149  grpnpncan0  13171  dfgrp3mlem  13173  grplactcnv  13177  mulgval  13195  mulgfng  13197  mulg1  13202  mulgnnp1  13203  mulgneg  13213  mulgnndir  13224  mulgdirlem  13226  mulgnn0ass  13231  mulgass  13232  subgmulg  13261  issubg4m  13266  subgintm  13271  0nsg  13287  eqgcpbl  13301  ghmmulg  13329  ghmpreima  13339  ghmeql  13340  ghmnsgima  13341  ghmnsgpreima  13342  ghmf1  13346  ghmf1o  13348  conjghm  13349  conjnmzb  13353  qusghm  13355  ablpncan3  13390  invghm  13402  eqgabl  13403  qusecsub  13404  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  imasrng  13455  qusrng  13457  srglmhm  13492  srgrmhm  13493  ringpropd  13537  ringlghm  13560  ringrghm  13561  imasring  13563  qusring2  13565  opprrngbg  13577  dvdsrvald  13592  dvdsrd  13593  dvdsrex  13597  dvdsrtr  13600  unitgrp  13615  unitpropdg  13647  rhmopp  13675  isnzr2  13683  issubrng2  13709  subrngintm  13711  subrgintm  13742  rhmpropd  13753  aprap  13785  lmodprop2d  13847  rmodislmodlem  13849  lssvacl  13864  lssvsubcl  13865  lssvscl  13874  islss3  13878  lsspropdg  13930  rnglidlmcl  13979  2idlcpblrng  14022  crngridl  14029  expghmap  14106  mulgghm2  14107  mulgrhm  14108  znf1o  14150  znleval  14152  znidom  14156  psrval  14163  epttop  14269  topssnei  14341  restbasg  14347  restopnb  14360  cnfval  14373  cnpfval  14374  iscnp4  14397  cnpnei  14398  cnptopco  14401  cncnp  14409  cnrest2  14415  cnptoprest  14418  cnptoprest2  14419  lmss  14425  lmtopcnp  14429  neitx  14447  txcnp  14450  txrest  14455  txdis  14456  txlm  14458  cnmpt21  14470  imasnopn  14478  xmetres2  14558  blvalps  14567  blval  14568  bl2in  14582  blhalf  14587  blssps  14606  blss  14607  blssexps  14608  blssex  14609  ssblex  14610  blin2  14611  metss2lem  14676  bdmetval  14679  bdmopn  14683  metrest  14685  xmetxp  14686  xmetxpbl  14687  xmettx  14689  metcnp3  14690  txmetcnp  14697  addcncntoplem  14740  elcncf2  14753  mulc1cncf  14768  cncfco  14770  cncfmet  14771  mulcncf  14787  dedekindeulemub  14797  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeu  14802  suplociccex  14804  dedekindicclemub  14806  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthdec  14823  ivthreinc  14824  dich0  14831  limcimolemlt  14843  limcimo  14844  cnplimccntop  14849  limccnp2lem  14855  limccnp2cntop  14856  dvfvalap  14860  dvmptfsum  14904  dveflem  14905  plyco  14937  plycn  14940  plyrecj  14941  reeff1olem  14947  reeff1oleme  14948  eflt  14951  sin0pilem2  14958  pilem3  14959  ptolemy  15000  ioocosf1o  15030  cxplt  15091  cxple  15092  cxplt3  15095  apcxp2  15113  rprelogbmul  15128  rprelogbdiv  15130  logbgt0b  15139  logbgcd1irrap  15143  lgsdir2lem5  15189  lgsdir  15192  lgsdi  15194  lgsne0  15195  gausslemma2dlem1f1o  15217  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  lgsquad2  15240  2sqlem6  15277  2sqlem10  15282  nnti  15555  pwtrufal  15558  pwf1oexmid  15560  sssneq  15562  qdencn  15587  cvgcmp2n  15593  trilpolemlt1  15601  trirec0  15604  trirec0xor  15605  redc0  15617  reap0  15618  cndcap  15619  nconstwlpolemgt0  15624  neap0mkv  15629  supfz  15631  inffz  15632