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  3090  disjiun  4038  reg3exmidlemwe  4626  0xp  4754  imainss  5097  iotam  5262  fvmptt  5670  fcof1o  5857  isotr  5884  riota5f  5923  ovmpodf  6076  unielxp  6259  fnmpoovd  6300  1stconst  6306  2ndconst  6307  cnvf1olem  6309  tfrlemi14d  6418  tfrexlem  6419  tfr1onlemres  6434  tfrcllemres  6447  tfrcldm  6448  frecabcl  6484  nnaordi  6593  swoer  6647  qliftfun  6703  ecopovsymg  6720  th3qlem1  6723  pw2f1odclem  6930  mapen  6942  mapxpen  6944  fidifsnen  6966  fisbth  6979  findcard2d  6987  findcard2sd  6988  diffisn  6989  diffifi  6990  ac6sfi  6994  fimax2gtri  6997  fientri3  7011  nnwetri  7012  unsnfi  7015  unsnfidcex  7016  unsnfidcel  7017  fisseneq  7030  fidcenumlemrk  7055  fidcenumlemr  7056  isbth  7068  ordiso2  7136  difinfsnlem  7200  difinfinf  7202  ctmlemr  7209  ctssdccl  7212  fodjum  7247  fodju0  7248  omniwomnimkv  7268  exmidfodomrlemrALT  7310  netap  7365  exmidmotap  7372  cc1  7376  cc2lem  7377  cc3  7379  cc4f  7380  cc4n  7382  dfplpq2  7466  dfmpq2  7467  mulpipqqs  7485  distrnqg  7499  ltexnqq  7520  subhalfnqq  7526  distrnq0  7571  prarloclemup  7607  prarloclem3  7609  prarloc  7615  genplt2i  7622  nqprl  7663  nqpru  7664  prmuloc  7678  mullocpr  7683  distrlem4prl  7696  distrlem4pru  7697  ltaddpr  7709  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  ltexprlemrl  7722  ltexprlemru  7724  addcanprleml  7726  addcanprlemu  7727  ltaprlem  7730  ltaprg  7731  prplnqu  7732  addextpr  7733  recexprlemdisj  7742  recexprlemloc  7743  recexprlem1ssl  7745  aptiprleml  7751  aptiprlemu  7752  ltmprr  7754  archpr  7755  cauappcvgprlemopl  7758  cauappcvgprlemopu  7760  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlem1  7771  cauappcvgprlem2  7772  cauappcvgprlemlim  7773  caucvgprlemnkj  7778  caucvgprlemopl  7781  caucvgprlemopu  7783  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlem2  7792  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemnjltk  7803  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemopu  7811  caucvgprprlemdisj  7814  caucvgprprlemloc  7815  caucvgprprlemexbt  7818  caucvgprprlemaddq  7820  caucvgprprlem2  7822  suplocexprlemrl  7829  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemex  7834  suplocexprlemub  7835  suplocexprlemlub  7836  recexgt0sr  7885  mulgt0sr  7890  prsrriota  7900  caucvgsrlemoffres  7912  suplocsrlem  7920  cnm  7944  addcnsr  7946  mulcnsr  7947  mulcnsrec  7955  axaddcl  7976  axmulcl  7978  axmulcom  7983  rereceu  8001  recriota  8002  axcaucvglemres  8011  axpre-suploclemres  8013  lelttr  8160  ltletr  8161  readdcan  8211  addcan  8251  addcan2  8252  addsub4  8314  ltadd2  8491  le2add  8516  lt2add  8517  lt2sub  8532  le2sub  8533  eqord1  8555  rimul  8657  rereim  8658  ltmul1  8664  apreim  8675  mulreim  8676  apcotr  8679  apadd1  8680  addext  8682  apneg  8683  mulext1  8684  mulext  8686  ltleap  8704  aprcl  8718  mulap0  8726  mulcanapd  8733  receuap  8741  recapb  8743  rec11ap  8782  rec11rap  8783  divdivdivap  8785  ddcanap  8798  divadddivap  8799  conjmulap  8801  subrecap  8911  prodgt0gt0  8923  prodge0  8926  ltmul12a  8932  lemulge11  8938  lt2mul2div  8951  ltrec  8955  lerec  8956  lt2msq  8958  lerec2  8961  le2msq  8973  msq11  8974  ledivp1  8975  mulle0r  9016  suprzclex  9470  peano5uzti  9480  supinfneg  9715  infsupneg  9716  qapne  9759  xrlelttr  9927  xrltletr  9928  xrre  9941  xaddge0  9999  xle2add  10000  xlt2add  10001  divelunit  10123  fzass4  10183  fzocatel  10326  zsupcllemstep  10370  zssinfcl  10373  suprzubdc  10377  zsupssdc  10379  suprzcl2dc  10380  exbtwnzlemex  10390  rebtwn2z  10395  qbtwnre  10397  modqid  10492  modqcyc  10502  modqaddabs  10505  modqaddmod  10506  mulqaddmodid  10507  modqadd2mod  10517  modqltm1p1mod  10519  modqsubmod  10525  modqsubmodmod  10526  modqmulmod  10532  modqmulmodr  10533  modqaddmulmod  10534  modqsubdir  10536  frec2uzisod  10550  iseqovex  10601  seqvalcd  10604  seq1g  10606  seqf  10607  seqovcd  10610  seqm1g  10617  seq3fveq2  10618  seq3shft2  10624  seqshft2g  10625  monoord  10628  seq3split  10631  seqsplitg  10632  iseqf1olemnab  10644  seqf1oglem1  10662  seqf1og  10664  seq3id2  10669  seqhomog  10673  seq3distr  10675  expcl2lemap  10694  expnegzap  10716  ltexp2a  10734  le2sq2  10758  nn0ltexp2  10852  nn0opth2  10867  bcval5  10906  hashcl  10924  hashen  10927  fihashdom  10946  hashunlem  10947  hashun  10948  fimaxq  10970  zfz1isolem1  10983  zfz1iso  10984  lencl  10996  sswrd  11001  fstwrdne0  11031  lswlgt0cl  11043  cvg1nlemres  11238  cvg1n  11239  recvguniq  11248  resqrexlemp1rp  11259  resqrexlemoverl  11274  resqrexlemglsq  11275  resqrexlemex  11278  sqrtmul  11288  sqrtsq  11297  absexpzap  11333  absle  11342  abs3lem  11364  amgm2  11371  maxleastlt  11468  maxltsup  11471  fimaxre2  11480  xrmaxleastlt  11509  xrmaxltsup  11511  xrmaxaddlem  11513  climcn2  11562  addcn2  11563  mulcn2  11565  reccn2ap  11566  climcau  11600  summodclem2  11635  summodc  11636  fsumf1o  11643  fisumss  11645  fsum3cvg3  11649  fsumcl2lem  11651  fsumadd  11659  fsum2dlemstep  11687  mptfzshft  11695  fsumrev  11696  fsummulc2  11701  modfsummod  11711  fsumrelem  11724  binom  11737  cvgratnn  11784  mertenslemub  11787  prodmodc  11831  zproddc  11832  fprodf1o  11841  fprodssdc  11843  fprodmul  11844  fprodrev  11872  fprod2dlemstep  11875  efcllem  11912  tanaddaplem  11991  dvdsval2  12043  moddvds  12052  dvdsabseq  12100  dvdsflip  12104  oexpneg  12130  fldivndvdslt  12190  bitsfi  12210  bezoutlemnewy  12259  bezoutlemstep  12260  bezoutlemeu  12270  dfgcd3  12273  bezout  12274  dvdsmulgcd  12288  bezoutr  12295  nninfctlemfo  12303  ialgrlem1st  12306  lcmgcdlem  12341  coprmdvds2  12357  qredeu  12361  rpdvds  12363  isprm5lem  12405  isprm6  12411  pw2dvdslemn  12429  nonsq  12471  crth  12488  eulerthlemh  12495  pclemdc  12553  pcprendvds2  12556  pceu  12560  pcval  12561  pczpre  12562  pcmul  12566  pcqmul  12568  pcqcl  12571  pcid  12589  pcneg  12590  pcgcd1  12593  pc2dvds  12595  pcprmpw2  12598  difsqpwdvds  12603  pcmpt  12608  pockthg  12622  1arith  12632  mul4sq  12659  4sqexercise2  12664  ennnfonelemg  12716  ennnfonelemex  12727  ennnfonelemrnh  12729  ennnfonelemrn  12732  ennnfonelemdm  12733  ennnfonelemnn0  12735  ennnfonelemim  12737  ennnfone  12738  ctinfomlemom  12740  ctinf  12743  ctiunctlemfo  12752  nninfdclemcl  12761  nninfdclemf  12762  nninfdclemp1  12763  unbendc  12767  isstruct2r  12785  setscom  12814  qusval  13097  ercpbl  13105  opifismgmdc  13145  grpinvalem  13159  grprida  13161  igsumvalx  13163  gsumfzval  13165  gsumpropd2  13167  gsumval2  13171  sgrppropd  13187  prdssgrpd  13189  mndpropd  13214  issubmnd  13216  submnd0  13218  prdsmndd  13222  mhmf1o  13244  0mhm  13260  resmhm  13261  mhmco  13264  mhmima  13265  mhmeql  13266  gsumwsubmcl  13270  gsumfzcl  13273  grppropd  13291  grpinvid1  13326  grpinvid2  13327  grplcan  13336  grplmulf1o  13348  grpnpncan0  13370  dfgrp3mlem  13372  grplactcnv  13376  pwssub  13387  mulgval  13400  mulgfng  13402  mulg1  13407  mulgnnp1  13408  mulgneg  13418  mulgnndir  13429  mulgdirlem  13431  mulgnn0ass  13436  mulgass  13437  subgmulg  13466  issubg4m  13471  subgintm  13476  0nsg  13492  eqgcpbl  13506  ghmmulg  13534  ghmpreima  13544  ghmeql  13545  ghmnsgima  13546  ghmnsgpreima  13547  ghmf1  13551  ghmf1o  13553  conjghm  13554  conjnmzb  13558  qusghm  13560  ablpncan3  13595  invghm  13607  eqgabl  13608  qusecsub  13609  gsumfzreidx  13615  gsumfzsubmcl  13616  gsumfzmptfidmadd  13617  gsumfzmhm  13621  imasrng  13660  qusrng  13662  srglmhm  13697  srgrmhm  13698  ringpropd  13742  ringlghm  13765  ringrghm  13766  imasring  13768  qusring2  13770  opprrngbg  13782  dvdsrvald  13797  dvdsrd  13798  dvdsrex  13802  dvdsrtr  13805  unitgrp  13820  unitpropdg  13852  rhmopp  13880  isnzr2  13888  issubrng2  13914  subrngintm  13916  subrgintm  13947  rhmpropd  13958  aprap  13990  lmodprop2d  14052  rmodislmodlem  14054  lssvacl  14069  lssvsubcl  14070  lssvscl  14079  islss3  14083  lsspropdg  14135  rnglidlmcl  14184  2idlcpblrng  14227  crngridl  14234  expghmap  14311  mulgghm2  14312  mulgrhm  14313  znf1o  14355  znleval  14357  znidom  14361  psrval  14370  mplsubgfilemcl  14403  epttop  14504  topssnei  14576  restbasg  14582  restopnb  14595  cnfval  14608  cnpfval  14609  iscnp4  14632  cnpnei  14633  cnptopco  14636  cncnp  14644  cnrest2  14650  cnptoprest  14653  cnptoprest2  14654  lmss  14660  lmtopcnp  14664  neitx  14682  txcnp  14685  txrest  14690  txdis  14691  txlm  14693  cnmpt21  14705  imasnopn  14713  xmetres2  14793  blvalps  14802  blval  14803  bl2in  14817  blhalf  14822  blssps  14841  blss  14842  blssexps  14843  blssex  14844  ssblex  14845  blin2  14846  metss2lem  14911  bdmetval  14914  bdmopn  14918  metrest  14920  xmetxp  14921  xmetxpbl  14922  xmettx  14924  metcnp3  14925  txmetcnp  14932  addcncntoplem  14975  elcncf2  14988  mulc1cncf  15003  cncfco  15005  cncfmet  15006  mulcncf  15022  dedekindeulemub  15032  dedekindeulemloc  15033  dedekindeulemlu  15035  dedekindeu  15037  suplociccex  15039  dedekindicclemub  15041  dedekindicclemloc  15042  dedekindicclemlu  15044  dedekindicc  15047  ivthinclemlopn  15050  ivthinclemuopn  15052  ivthdec  15058  ivthreinc  15059  dich0  15066  limcimolemlt  15078  limcimo  15079  cnplimccntop  15084  limccnp2lem  15090  limccnp2cntop  15091  dvfvalap  15095  dvmptfsum  15139  dveflem  15140  plyco  15173  plycn  15176  plyrecj  15177  reeff1olem  15185  reeff1oleme  15186  eflt  15189  sin0pilem2  15196  pilem3  15197  ptolemy  15238  ioocosf1o  15268  cxplt  15330  cxple  15331  cxplt3  15334  apcxp2  15353  rprelogbmul  15369  rprelogbdiv  15371  logbgt0b  15380  logbgcd1irrap  15384  fsumdvdsmul  15405  perfectlem2  15414  lgsdir2lem5  15451  lgsdir  15454  lgsdi  15456  lgsne0  15457  gausslemma2dlem1f1o  15479  lgseisenlem2  15490  lgsquadlem1  15496  lgsquadlem2  15497  lgsquad2lem2  15501  lgsquad2  15502  2sqlem6  15539  2sqlem10  15544  nnti  15862  pwtrufal  15867  pwf1oexmid  15869  sssneq  15872  qdencn  15899  cvgcmp2n  15905  trilpolemlt1  15913  trirec0  15916  trirec0xor  15917  redc0  15929  reap0  15930  cndcap  15931  nconstwlpolemgt0  15936  neap0mkv  15941  supfz  15943  inffz  15944