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  989  simp1rl  1088  simp2rl  1092  simp3rl  1096  rmob  3125  elpr2elpr  3859  disjiun  4083  reg3exmidlemwe  4677  opabssxpd  4762  0xp  4806  imainss  5152  iotam  5318  fvmptt  5738  fcof1o  5930  isotr  5957  riota5f  5998  ovmpodf  6153  unielxp  6337  fnmpoovd  6380  1stconst  6386  2ndconst  6387  cnvf1olem  6389  tfrlemi14d  6499  tfrexlem  6500  tfr1onlemres  6515  tfrcllemres  6528  tfrcldm  6529  frecabcl  6565  nnaordi  6676  swoer  6730  qliftfun  6786  ecopovsymg  6803  th3qlem1  6806  pw2f1odclem  7020  mapen  7032  mapxpen  7034  fidifsnen  7057  fisbth  7072  findcard2d  7080  findcard2sd  7081  diffisn  7082  diffifi  7083  ac6sfi  7087  fidcen  7088  fimax2gtri  7091  fientri3  7107  nnwetri  7108  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fisseneq  7127  exmidssfi  7131  fidcenumlemrk  7153  fidcenumlemr  7154  isbth  7166  ordiso2  7234  difinfsnlem  7298  difinfinf  7300  ctmlemr  7307  ctssdccl  7310  fodjum  7345  fodju0  7346  omniwomnimkv  7366  exmidfodomrlemrALT  7414  netap  7473  exmidmotap  7480  cc1  7484  cc2lem  7485  cc3  7487  cc4f  7488  cc4n  7490  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  distrnqg  7607  ltexnqq  7628  subhalfnqq  7634  distrnq0  7679  prarloclemup  7715  prarloclem3  7717  prarloc  7723  genplt2i  7730  nqprl  7771  nqpru  7772  prmuloc  7786  mullocpr  7791  distrlem4prl  7804  distrlem4pru  7805  ltaddpr  7817  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprlem  7838  ltaprg  7839  prplnqu  7840  addextpr  7841  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssl  7853  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  archpr  7863  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlem2  7900  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemdisj  7922  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  caucvgprprlem2  7930  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  suplocexprlemlub  7944  recexgt0sr  7993  mulgt0sr  7998  prsrriota  8008  caucvgsrlemoffres  8020  suplocsrlem  8028  cnm  8052  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axaddcl  8084  axmulcl  8086  axmulcom  8091  rereceu  8109  recriota  8110  axcaucvglemres  8119  axpre-suploclemres  8121  lelttr  8268  ltletr  8269  readdcan  8319  addcan  8359  addcan2  8360  addsub4  8422  ltadd2  8599  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  eqord1  8663  rimul  8765  rereim  8766  ltmul1  8772  apreim  8783  mulreim  8784  apcotr  8787  apadd1  8788  addext  8790  apneg  8791  mulext1  8792  mulext  8794  ltleap  8812  aprcl  8826  mulap0  8834  mulcanapd  8841  receuap  8849  recapb  8851  rec11ap  8890  rec11rap  8891  divdivdivap  8893  ddcanap  8906  divadddivap  8907  conjmulap  8909  subrecap  9019  prodgt0gt0  9031  prodge0  9034  ltmul12a  9040  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  lt2msq  9066  lerec2  9069  le2msq  9081  msq11  9082  ledivp1  9083  mulle0r  9124  suprzclex  9578  peano5uzti  9588  supinfneg  9829  infsupneg  9830  qapne  9873  xrlelttr  10041  xrltletr  10042  xrre  10055  xaddge0  10113  xle2add  10114  xlt2add  10115  divelunit  10237  fzass4  10297  fzocatel  10445  zsupcllemstep  10490  zssinfcl  10493  suprzubdc  10497  zsupssdc  10499  suprzcl2dc  10500  exbtwnzlemex  10510  rebtwn2z  10515  qbtwnre  10517  modqid  10612  modqcyc  10622  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqadd2mod  10637  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modqmulmod  10652  modqmulmodr  10653  modqaddmulmod  10654  modqsubdir  10656  frec2uzisod  10670  iseqovex  10721  seqvalcd  10724  seq1g  10726  seqf  10727  seqovcd  10730  seqm1g  10737  seq3fveq2  10738  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  iseqf1olemnab  10764  seqf1oglem1  10782  seqf1og  10784  seq3id2  10789  seqhomog  10793  seq3distr  10795  expcl2lemap  10814  expnegzap  10836  ltexp2a  10854  le2sq2  10878  nn0ltexp2  10972  nn0opth2  10987  bcval5  11026  hashcl  11044  hashen  11047  fihashdom  11067  hashunlem  11068  hashun  11069  fimaxq  11092  zfz1isolem1  11105  zfz1iso  11106  lencl  11121  sswrd  11126  fstwrdne0  11157  lswlgt0cl  11170  ccatw2s1p1g  11226  ccat2s1fstg  11229  swrdval  11233  wrdind  11307  wrd2ind  11308  swrdccatfn  11309  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  pfxccat3a  11323  reuccatpfxs1  11332  cvg1nlemres  11550  cvg1n  11551  recvguniq  11560  resqrexlemp1rp  11571  resqrexlemoverl  11586  resqrexlemglsq  11587  resqrexlemex  11590  sqrtmul  11600  sqrtsq  11609  absexpzap  11645  absle  11654  abs3lem  11676  amgm2  11683  maxleastlt  11780  maxltsup  11783  fimaxre2  11792  xrmaxleastlt  11821  xrmaxltsup  11823  xrmaxaddlem  11825  climcn2  11874  addcn2  11875  mulcn2  11877  reccn2ap  11878  climcau  11912  summodclem2  11948  summodc  11949  fsumf1o  11956  fisumss  11958  fsum3cvg3  11962  fsumcl2lem  11964  fsumadd  11972  fsum2dlemstep  12000  mptfzshft  12008  fsumrev  12009  fsummulc2  12014  modfsummod  12024  fsumrelem  12037  binom  12050  cvgratnn  12097  mertenslemub  12100  prodmodc  12144  zproddc  12145  fprodf1o  12154  fprodssdc  12156  fprodmul  12157  fprodrev  12185  fprod2dlemstep  12188  efcllem  12225  tanaddaplem  12304  dvdsval2  12356  moddvds  12365  dvdsabseq  12413  dvdsflip  12417  oexpneg  12443  fldivndvdslt  12503  bitsfi  12523  bezoutlemnewy  12572  bezoutlemstep  12573  bezoutlemeu  12583  dfgcd3  12586  bezout  12587  dvdsmulgcd  12601  bezoutr  12608  nninfctlemfo  12616  ialgrlem1st  12619  lcmgcdlem  12654  coprmdvds2  12670  qredeu  12674  rpdvds  12676  isprm5lem  12718  isprm6  12724  pw2dvdslemn  12742  nonsq  12784  crth  12801  eulerthlemh  12808  pclemdc  12866  pcprendvds2  12869  pceu  12873  pcval  12874  pczpre  12875  pcmul  12879  pcqmul  12881  pcqcl  12884  pcid  12902  pcneg  12903  pcgcd1  12906  pc2dvds  12908  pcprmpw2  12911  difsqpwdvds  12916  pcmpt  12921  pockthg  12935  1arith  12945  mul4sq  12972  4sqexercise2  12977  ennnfonelemg  13029  ennnfonelemex  13040  ennnfonelemrnh  13042  ennnfonelemrn  13045  ennnfonelemdm  13046  ennnfonelemnn0  13048  ennnfonelemim  13050  ennnfone  13051  ctinfomlemom  13053  ctinf  13056  ctiunctlemfo  13065  nninfdclemcl  13074  nninfdclemf  13075  nninfdclemp1  13076  unbendc  13080  isstruct2r  13098  setscom  13127  qusval  13411  ercpbl  13419  opifismgmdc  13459  grpinvalem  13473  grprida  13475  igsumvalx  13477  gsumfzval  13479  gsumpropd2  13481  gsumval2  13485  sgrppropd  13501  prdssgrpd  13503  mndpropd  13528  issubmnd  13530  submnd0  13532  prdsmndd  13536  mhmf1o  13558  0mhm  13574  resmhm  13575  mhmco  13578  mhmima  13579  mhmeql  13580  gsumwsubmcl  13584  gsumfzcl  13587  grppropd  13605  grpinvid1  13640  grpinvid2  13641  grplcan  13650  grplmulf1o  13662  grpnpncan0  13684  dfgrp3mlem  13686  grplactcnv  13690  pwssub  13701  mulgval  13714  mulgfng  13716  mulg1  13721  mulgnnp1  13722  mulgneg  13732  mulgnndir  13743  mulgdirlem  13745  mulgnn0ass  13750  mulgass  13751  subgmulg  13780  issubg4m  13785  subgintm  13790  0nsg  13806  eqgcpbl  13820  ghmmulg  13848  ghmpreima  13858  ghmeql  13859  ghmnsgima  13860  ghmnsgpreima  13861  ghmf1  13865  ghmf1o  13867  conjghm  13868  conjnmzb  13872  qusghm  13874  ablpncan3  13909  invghm  13921  eqgabl  13922  qusecsub  13923  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  imasrng  13975  qusrng  13977  srglmhm  14012  srgrmhm  14013  ringpropd  14057  ringlghm  14080  ringrghm  14081  imasring  14083  qusring2  14085  opprrngbg  14097  dvdsrvald  14113  dvdsrd  14114  dvdsrex  14118  dvdsrtr  14121  unitgrp  14136  unitpropdg  14168  rhmopp  14196  isnzr2  14204  issubrng2  14230  subrngintm  14232  subrgintm  14263  rhmpropd  14274  aprap  14306  lmodprop2d  14368  rmodislmodlem  14370  lssvacl  14385  lssvsubcl  14386  lssvscl  14395  islss3  14399  lsspropdg  14451  rnglidlmcl  14500  2idlcpblrng  14543  crngridl  14550  expghmap  14627  mulgghm2  14628  mulgrhm  14629  znf1o  14671  znleval  14673  znidom  14677  psrval  14686  mplsubgfilemcl  14719  epttop  14820  topssnei  14892  restbasg  14898  restopnb  14911  cnfval  14924  cnpfval  14925  iscnp4  14948  cnpnei  14949  cnptopco  14952  cncnp  14960  cnrest2  14966  cnptoprest  14969  cnptoprest2  14970  lmss  14976  lmtopcnp  14980  neitx  14998  txcnp  15001  txrest  15006  txdis  15007  txlm  15009  cnmpt21  15021  imasnopn  15029  xmetres2  15109  blvalps  15118  blval  15119  bl2in  15133  blhalf  15138  blssps  15157  blss  15158  blssexps  15159  blssex  15160  ssblex  15161  blin2  15162  metss2lem  15227  bdmetval  15230  bdmopn  15234  metrest  15236  xmetxp  15237  xmetxpbl  15238  xmettx  15240  metcnp3  15241  txmetcnp  15248  addcncntoplem  15291  elcncf2  15304  mulc1cncf  15319  cncfco  15321  cncfmet  15322  mulcncf  15338  dedekindeulemub  15348  dedekindeulemloc  15349  dedekindeulemlu  15351  dedekindeu  15353  suplociccex  15355  dedekindicclemub  15357  dedekindicclemloc  15358  dedekindicclemlu  15360  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthdec  15374  ivthreinc  15375  dich0  15382  limcimolemlt  15394  limcimo  15395  cnplimccntop  15400  limccnp2lem  15406  limccnp2cntop  15407  dvfvalap  15411  dvmptfsum  15455  dveflem  15456  plyco  15489  plycn  15492  plyrecj  15493  reeff1olem  15501  reeff1oleme  15502  eflt  15505  sin0pilem2  15512  pilem3  15513  ptolemy  15554  ioocosf1o  15584  cxplt  15646  cxple  15647  cxplt3  15650  apcxp2  15669  rprelogbmul  15685  rprelogbdiv  15687  logbgt0b  15696  logbgcd1irrap  15700  fsumdvdsmul  15721  perfectlem2  15730  lgsdir2lem5  15767  lgsdir  15770  lgsdi  15772  lgsne0  15773  gausslemma2dlem1f1o  15795  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem2  15817  lgsquad2  15818  2sqlem6  15855  2sqlem10  15860  upgredg  16001  uhgrissubgr  16118  subgrprop3  16119  upgrspanop  16140  umgrspanop  16141  usgrspanop  16142  vtxedgfi  16146  vtxlpfi  16147  upgr2wlkdc  16234  clwwlkccatlem  16257  eupth2lemsfi  16335  depindlem3  16353  nnti  16617  pwtrufal  16624  pwf1oexmid  16626  sssneq  16629  qdencn  16657  cvgcmp2n  16663  trilpolemlt1  16671  trirec0  16674  trirec0xor  16675  qdiff  16679  redc0  16688  reap0  16689  cndcap  16690  nconstwlpolemgt0  16695  neap0mkv  16700  supfz  16702  inffz  16703  gfsumval  16707  gfsumcl  16714