Theorem simprl 531

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  990  simp1rl  1089  simp2rl  1093  simp3rl  1097  rmob  3139  elpr2elpr  3885  disjiun  4109  reg3exmidlemwe  4706  opabssxpd  4791  0xp  4835  imainss  5183  iotam  5349  fvmptt  5774  fcof1o  5968  isotr  5995  riota5f  6038  ovmpodf  6193  unielxp  6381  fnmpoovd  6424  1stconst  6430  2ndconst  6431  cnvf1olem  6433  fvn0elsupp  6464  suppcofn  6479  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemres  6593  tfrcllemres  6606  tfrcldm  6607  frecabcl  6643  nnaordi  6754  swoer  6808  qliftfun  6864  ecopovsymg  6881  th3qlem1  6884  pw2f1odclem  7100  mapen  7112  mapxpen  7114  fidifsnen  7138  fisbth  7153  findcard2d  7161  findcard2sd  7162  diffisn  7163  diffifi  7164  ac6sfi  7168  fidcen  7169  fimax2gtri  7172  fientri3  7188  nnwetri  7189  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  fisseneq  7208  exmidssfi  7212  fidcenumlemrk  7237  fidcenumlemr  7238  isbth  7250  ordiso2  7339  difinfsnlem  7403  difinfinf  7405  ctmlemr  7412  ctssdccl  7415  fodjum  7450  fodju0  7451  omniwomnimkv  7471  exmidfodomrlemrALT  7519  netap  7584  exmidmotap  7591  cc1  7595  cc2lem  7596  cc3  7598  cc4f  7599  cc4n  7601  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  distrnqg  7718  ltexnqq  7739  subhalfnqq  7745  distrnq0  7790  prarloclemup  7826  prarloclem3  7828  prarloc  7834  genplt2i  7841  nqprl  7882  nqpru  7883  prmuloc  7897  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltaddpr  7928  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltaprlem  7949  ltaprg  7950  prplnqu  7951  addextpr  7952  recexprlemdisj  7961  recexprlemloc  7962  recexprlem1ssl  7964  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  archpr  7974  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlem1  7990  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlem2  8011  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnjltk  8022  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlem2  8041  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  suplocexprlemlub  8055  recexgt0sr  8104  mulgt0sr  8109  prsrriota  8119  caucvgsrlemoffres  8131  suplocsrlem  8139  cnm  8163  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axaddcl  8195  axmulcl  8197  axmulcom  8202  rereceu  8220  recriota  8221  axcaucvglemres  8230  axpre-suploclemres  8232  lelttr  8378  ltletr  8379  readdcan  8429  addcan  8469  addcan2  8470  addsub4  8532  ltadd2  8710  le2add  8735  lt2add  8736  lt2sub  8751  le2sub  8752  eqord1  8774  rimul  8876  rereim  8877  ltmul1  8883  apreim  8894  mulreim  8895  apcotr  8898  apadd1  8899  addext  8901  apneg  8902  mulext1  8903  mulext  8905  ltleap  8923  aprcl  8937  mulap0  8945  mulcanapd  8952  receuap  8960  recapb  8962  rec11ap  9001  rec11rap  9002  divdivdivap  9004  ddcanap  9017  divadddivap  9018  conjmulap  9020  subrecap  9130  prodgt0gt0  9142  prodge0  9145  ltmul12a  9151  lemulge11  9157  lt2mul2div  9170  ltrec  9174  lerec  9175  lt2msq  9177  lerec2  9180  le2msq  9192  msq11  9193  ledivp1  9194  mulle0r  9235  suprzclex  9694  peano5uzti  9704  supinfneg  9945  infsupneg  9946  qapne  9989  xrlelttr  10158  xrltletr  10159  xrre  10172  xaddge0  10230  xle2add  10231  xlt2add  10232  divelunit  10354  fzass4  10417  fzocatel  10566  zsupcllemstep  10611  zssinfcl  10614  infssfzcldc  10618  infssfzledc  10619  suprzubdc  10620  zsupssdc  10622  suprzcl2dc  10623  exbtwnzlemex  10633  rebtwn2z  10638  qbtwnre  10640  modqid  10735  modqcyc  10745  modqaddabs  10748  modqaddmod  10749  mulqaddmodid  10750  modqadd2mod  10760  modqltm1p1mod  10762  modqsubmod  10768  modqsubmodmod  10769  modqmulmod  10775  modqmulmodr  10776  modqaddmulmod  10777  modqsubdir  10779  frec2uzisod  10793  iseqovex  10844  seqvalcd  10847  seq1g  10849  seqf  10850  seqovcd  10853  seqm1g  10860  seq3fveq2  10861  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  iseqf1olemnab  10887  seqf1oglem1  10905  seqf1og  10907  seq3id2  10912  seqhomog  10916  seq3distr  10918  expcl2lemap  10937  expnegzap  10959  ltexp2a  10977  le2sq2  11001  nn0ltexp2  11096  nn0opth2  11111  bcval5  11150  hashcl  11169  hashen  11172  fihashdom  11192  hashunlem  11193  hashun  11194  hashmap  11217  fimaxq  11219  hashfibclem  11231  hashfibc  11232  zfz1isolem1  11237  zfz1iso  11238  lencl  11253  sswrd  11258  fstwrdne0  11289  lswlgt0cl  11302  ccatw2s1p1g  11358  ccat2s1fstg  11361  swrdval  11365  wrdind  11439  wrd2ind  11440  swrdccatfn  11441  swrdccatin1  11442  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  pfxccat3a  11455  reuccatpfxs1  11464  cvg1nlemres  11695  cvg1n  11696  recvguniq  11705  resqrexlemp1rp  11716  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemex  11735  sqrtmul  11745  sqrtsq  11754  absexpzap  11790  absle  11799  abs3lem  11821  amgm2  11828  maxleastlt  11925  maxltsup  11928  fimaxre2  11937  xrmaxleastlt  11966  xrmaxltsup  11968  xrmaxaddlem  11970  climcn2  12019  addcn2  12020  mulcn2  12022  reccn2ap  12023  climcau  12057  summodclem2  12093  summodc  12094  fsumf1o  12101  fisumss  12103  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  fsum2dlemstep  12145  mptfzshft  12153  fsumrev  12154  fsummulc2  12159  modfsummod  12169  fsumrelem  12182  binom  12195  cvgratnn  12242  mertenslemub  12245  prodmodc  12289  zproddc  12290  fprodf1o  12299  fprodssdc  12301  fprodmul  12302  fprodrev  12330  fprod2dlemstep  12333  efcllem  12370  tanaddaplem  12449  dvdsval2  12501  moddvds  12510  dvdsabseq  12558  dvdsflip  12562  oexpneg  12588  fldivndvdslt  12648  bitsfi  12668  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemeu  12728  dfgcd3  12731  bezout  12732  dvdsmulgcd  12746  bezoutr  12753  nninfctlemfo  12761  ialgrlem1st  12764  lcmgcdlem  12799  coprmdvds2  12815  qredeu  12819  rpdvds  12821  isprm5lem  12863  isprm6  12869  pw2dvdslemn  12887  nonsq  12929  crth  12946  eulerthlemh  12953  pclemdc  13011  pcprendvds2  13014  pceu  13018  pcval  13019  pczpre  13020  pcmul  13024  pcqmul  13026  pcqcl  13029  pcid  13047  pcneg  13048  pcgcd1  13051  pc2dvds  13053  pcprmpw2  13056  difsqpwdvds  13061  pcmpt  13066  pockthg  13080  1arith  13090  mul4sq  13117  4sqexercise2  13122  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemg  13238  ennnfonelemex  13249  ennnfonelemrnh  13251  ennnfonelemrn  13254  ennnfonelemdm  13255  ennnfonelemnn0  13257  ennnfonelemim  13259  ennnfone  13260  ctinfomlemom  13262  ctinf  13265  ctiunctlemfo  13274  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  unbendc  13289  isstruct2r  13307  setscom  13336  qusval  13587  ercpbl  13595  opifismgmdc  13634  grpinvalem  13648  grprida  13650  igsumvalx  13652  gsumfzval  13654  gsumpropd2  13656  gsumval2  13660  sgrppropd  13676  mndpropd  13701  issubmnd  13703  submnd0  13705  mhmf1o  13725  0mhm  13741  resmhm  13742  mhmco  13745  mhmima  13746  mhmeql  13747  gsumwsubmcl  13751  gsumfzcl  13754  grppropd  13772  grpinvid1  13807  grpinvid2  13808  grplcan  13817  grplmulf1o  13829  grpnpncan0  13851  dfgrp3mlem  13853  grplactcnv  13857  mulgval  13875  mulgfng  13877  mulg1  13882  mulgnnp1  13883  mulgneg  13893  mulgnndir  13904  mulgdirlem  13906  mulgnn0ass  13911  mulgass  13912  subgmulg  13941  issubg4m  13946  subgintm  13951  0nsg  13967  eqgcpbl  13981  ghmmulg  14009  ghmpreima  14019  ghmeql  14020  ghmnsgima  14021  ghmnsgpreima  14022  ghmf1  14026  ghmf1o  14028  conjghm  14029  conjnmzb  14033  qusghm  14035  ablpncan3  14070  invghm  14082  eqgabl  14083  qusecsub  14084  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  gfsumval  14102  gfsumcl  14110  prdssgrpd  14133  prdsmndd  14136  pwssub  14158  imasrng  14195  qusrng  14197  srglmhm  14236  srgrmhm  14237  ringpropd  14281  ringlghm  14304  ringrghm  14305  imasring  14307  qusring2  14309  opprrngbg  14321  dvdsrvald  14338  dvdsrd  14339  dvdsrex  14343  dvdsrtr  14346  unitgrp  14361  unitpropdg  14393  rhmopp  14421  isnzr2  14429  issubrng2  14456  subrngintm  14458  subrgintm  14489  rhmpropd  14500  ringunitap  14531  aprap  14536  drngunitap  14546  lmodprop2d  14622  rmodislmodlem  14624  lssvacl  14639  lssvsubcl  14640  lssvscl  14649  islss3  14653  lsspropdg  14705  rnglidlmcl  14754  2idlcpblrng  14797  crngridl  14804  expghmap  14881  mulgghm2  14882  mulgrhm  14883  znf1o  14925  znleval  14927  znidom  14931  psrval  14940  psrbagcon  14952  psrbagconf1o  14954  mplsubgfilemcl  14980  epttop  15081  topssnei  15153  restbasg  15159  restopnb  15172  cnfval  15185  cnpfval  15186  iscnp4  15209  cnpnei  15210  cnptopco  15213  cncnp  15221  cnrest2  15227  cnptoprest  15230  cnptoprest2  15231  lmss  15237  lmtopcnp  15241  neitx  15259  txcnp  15262  txrest  15267  txdis  15268  txlm  15270  cnmpt21  15282  imasnopn  15290  xmetres2  15370  blvalps  15379  blval  15380  bl2in  15394  blhalf  15399  blssps  15418  blss  15419  blssexps  15420  blssex  15421  ssblex  15422  blin2  15423  metss2lem  15488  bdmetval  15491  bdmopn  15495  metrest  15497  xmetxp  15498  xmetxpbl  15499  xmettx  15501  metcnp3  15502  txmetcnp  15509  addcncntoplem  15552  elcncf2  15565  mulc1cncf  15580  cncfco  15582  cncfmet  15583  mulcncf  15599  dedekindeulemub  15609  dedekindeulemloc  15610  dedekindeulemlu  15612  dedekindeu  15614  suplociccex  15616  dedekindicclemub  15618  dedekindicclemloc  15619  dedekindicclemlu  15621  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthdec  15635  ivthreinc  15636  dich0  15643  limcimolemlt  15655  limcimo  15656  cnplimccntop  15661  limccnp2lem  15667  limccnp2cntop  15668  dvfvalap  15672  dvmptfsum  15716  dveflem  15717  plyco  15750  plycn  15753  plyrecj  15754  reeff1olem  15762  reeff1oleme  15763  eflt  15766  sin0pilem2  15773  pilem3  15774  ptolemy  15815  ioocosf1o  15845  cxplt  15907  cxple  15908  cxplt3  15911  apcxp2  15930  rprelogbmul  15946  rprelogbdiv  15948  logbgt0b  15957  logbgcd1irrap  15961  pellexlem3  15973  fsumdvdsmul  15985  perfectlem2  15994  lgsdir2lem5  16031  lgsdir  16034  lgsdi  16036  lgsne0  16037  gausslemma2dlem1f1o  16059  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  lgsquad2  16082  2sqlem6  16119  2sqlem10  16124  upgredg  16265  uhgrissubgr  16382  subgrprop3  16383  upgrspanop  16404  umgrspanop  16405  usgrspanop  16406  vtxedgfi  16410  vtxlpfi  16411  upgr2wlkdc  16498  clwwlkccatlem  16521  eupth2lemsfi  16599  depindlem3  16629  nnti  16892  pwtrufal  16897  pwf1oexmid  16899  sssneq  16902  qdencn  16933  cvgcmp2n  16943  trilpolemlt1  16951  trirec0  16954  trirec0xor  16955  qdiff  16959  redc0  16968  reap0  16969  cndcap  16970  trimul0or  16971  nconstwlpolemgt0  16976  neap0mkv  16981  supfz  16983  inffz  16984