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  10444  zsupcllemstep  10489  zssinfcl  10492  suprzubdc  10496  zsupssdc  10498  suprzcl2dc  10499  exbtwnzlemex  10509  rebtwn2z  10514  qbtwnre  10516  modqid  10611  modqcyc  10621  modqaddabs  10624  modqaddmod  10625  mulqaddmodid  10626  modqadd2mod  10636  modqltm1p1mod  10638  modqsubmod  10644  modqsubmodmod  10645  modqmulmod  10651  modqmulmodr  10652  modqaddmulmod  10653  modqsubdir  10655  frec2uzisod  10669  iseqovex  10720  seqvalcd  10723  seq1g  10725  seqf  10726  seqovcd  10729  seqm1g  10736  seq3fveq2  10737  seq3shft2  10743  seqshft2g  10744  monoord  10747  seq3split  10750  seqsplitg  10751  iseqf1olemnab  10763  seqf1oglem1  10781  seqf1og  10783  seq3id2  10788  seqhomog  10792  seq3distr  10794  expcl2lemap  10813  expnegzap  10835  ltexp2a  10853  le2sq2  10877  nn0ltexp2  10971  nn0opth2  10986  bcval5  11025  hashcl  11043  hashen  11046  fihashdom  11066  hashunlem  11067  hashun  11068  fimaxq  11091  zfz1isolem1  11104  zfz1iso  11105  lencl  11117  sswrd  11122  fstwrdne0  11153  lswlgt0cl  11166  ccatw2s1p1g  11222  ccat2s1fstg  11225  swrdval  11229  wrdind  11303  wrd2ind  11304  swrdccatfn  11305  swrdccatin1  11306  swrdccatin2  11310  pfxccatin12lem2  11312  pfxccatin12  11314  pfxccat3a  11319  reuccatpfxs1  11328  cvg1nlemres  11546  cvg1n  11547  recvguniq  11556  resqrexlemp1rp  11567  resqrexlemoverl  11582  resqrexlemglsq  11583  resqrexlemex  11586  sqrtmul  11596  sqrtsq  11605  absexpzap  11641  absle  11650  abs3lem  11672  amgm2  11679  maxleastlt  11776  maxltsup  11779  fimaxre2  11788  xrmaxleastlt  11817  xrmaxltsup  11819  xrmaxaddlem  11821  climcn2  11870  addcn2  11871  mulcn2  11873  reccn2ap  11874  climcau  11908  summodclem2  11944  summodc  11945  fsumf1o  11952  fisumss  11954  fsum3cvg3  11958  fsumcl2lem  11960  fsumadd  11968  fsum2dlemstep  11996  mptfzshft  12004  fsumrev  12005  fsummulc2  12010  modfsummod  12020  fsumrelem  12033  binom  12046  cvgratnn  12093  mertenslemub  12096  prodmodc  12140  zproddc  12141  fprodf1o  12150  fprodssdc  12152  fprodmul  12153  fprodrev  12181  fprod2dlemstep  12184  efcllem  12221  tanaddaplem  12300  dvdsval2  12352  moddvds  12361  dvdsabseq  12409  dvdsflip  12413  oexpneg  12439  fldivndvdslt  12499  bitsfi  12519  bezoutlemnewy  12568  bezoutlemstep  12569  bezoutlemeu  12579  dfgcd3  12582  bezout  12583  dvdsmulgcd  12597  bezoutr  12604  nninfctlemfo  12612  ialgrlem1st  12615  lcmgcdlem  12650  coprmdvds2  12666  qredeu  12670  rpdvds  12672  isprm5lem  12714  isprm6  12720  pw2dvdslemn  12738  nonsq  12780  crth  12797  eulerthlemh  12804  pclemdc  12862  pcprendvds2  12865  pceu  12869  pcval  12870  pczpre  12871  pcmul  12875  pcqmul  12877  pcqcl  12880  pcid  12898  pcneg  12899  pcgcd1  12902  pc2dvds  12904  pcprmpw2  12907  difsqpwdvds  12912  pcmpt  12917  pockthg  12931  1arith  12941  mul4sq  12968  4sqexercise2  12973  ennnfonelemg  13025  ennnfonelemex  13036  ennnfonelemrnh  13038  ennnfonelemrn  13041  ennnfonelemdm  13042  ennnfonelemnn0  13044  ennnfonelemim  13046  ennnfone  13047  ctinfomlemom  13049  ctinf  13052  ctiunctlemfo  13061  nninfdclemcl  13070  nninfdclemf  13071  nninfdclemp1  13072  unbendc  13076  isstruct2r  13094  setscom  13123  qusval  13407  ercpbl  13415  opifismgmdc  13455  grpinvalem  13469  grprida  13471  igsumvalx  13473  gsumfzval  13475  gsumpropd2  13477  gsumval2  13481  sgrppropd  13497  prdssgrpd  13499  mndpropd  13524  issubmnd  13526  submnd0  13528  prdsmndd  13532  mhmf1o  13554  0mhm  13570  resmhm  13571  mhmco  13574  mhmima  13575  mhmeql  13576  gsumwsubmcl  13580  gsumfzcl  13583  grppropd  13601  grpinvid1  13636  grpinvid2  13637  grplcan  13646  grplmulf1o  13658  grpnpncan0  13680  dfgrp3mlem  13682  grplactcnv  13686  pwssub  13697  mulgval  13710  mulgfng  13712  mulg1  13717  mulgnnp1  13718  mulgneg  13728  mulgnndir  13739  mulgdirlem  13741  mulgnn0ass  13746  mulgass  13747  subgmulg  13776  issubg4m  13781  subgintm  13786  0nsg  13802  eqgcpbl  13816  ghmmulg  13844  ghmpreima  13854  ghmeql  13855  ghmnsgima  13856  ghmnsgpreima  13857  ghmf1  13861  ghmf1o  13863  conjghm  13864  conjnmzb  13868  qusghm  13870  ablpncan3  13905  invghm  13917  eqgabl  13918  qusecsub  13919  gsumfzreidx  13925  gsumfzsubmcl  13926  gsumfzmptfidmadd  13927  gsumfzmhm  13931  imasrng  13971  qusrng  13973  srglmhm  14008  srgrmhm  14009  ringpropd  14053  ringlghm  14076  ringrghm  14077  imasring  14079  qusring2  14081  opprrngbg  14093  dvdsrvald  14109  dvdsrd  14110  dvdsrex  14114  dvdsrtr  14117  unitgrp  14132  unitpropdg  14164  rhmopp  14192  isnzr2  14200  issubrng2  14226  subrngintm  14228  subrgintm  14259  rhmpropd  14270  aprap  14302  lmodprop2d  14364  rmodislmodlem  14366  lssvacl  14381  lssvsubcl  14382  lssvscl  14391  islss3  14395  lsspropdg  14447  rnglidlmcl  14496  2idlcpblrng  14539  crngridl  14546  expghmap  14623  mulgghm2  14624  mulgrhm  14625  znf1o  14667  znleval  14669  znidom  14673  psrval  14682  mplsubgfilemcl  14715  epttop  14816  topssnei  14888  restbasg  14894  restopnb  14907  cnfval  14920  cnpfval  14921  iscnp4  14944  cnpnei  14945  cnptopco  14948  cncnp  14956  cnrest2  14962  cnptoprest  14965  cnptoprest2  14966  lmss  14972  lmtopcnp  14976  neitx  14994  txcnp  14997  txrest  15002  txdis  15003  txlm  15005  cnmpt21  15017  imasnopn  15025  xmetres2  15105  blvalps  15114  blval  15115  bl2in  15129  blhalf  15134  blssps  15153  blss  15154  blssexps  15155  blssex  15156  ssblex  15157  blin2  15158  metss2lem  15223  bdmetval  15226  bdmopn  15230  metrest  15232  xmetxp  15233  xmetxpbl  15234  xmettx  15236  metcnp3  15237  txmetcnp  15244  addcncntoplem  15287  elcncf2  15300  mulc1cncf  15315  cncfco  15317  cncfmet  15318  mulcncf  15334  dedekindeulemub  15344  dedekindeulemloc  15345  dedekindeulemlu  15347  dedekindeu  15349  suplociccex  15351  dedekindicclemub  15353  dedekindicclemloc  15354  dedekindicclemlu  15356  dedekindicc  15359  ivthinclemlopn  15362  ivthinclemuopn  15364  ivthdec  15370  ivthreinc  15371  dich0  15378  limcimolemlt  15390  limcimo  15391  cnplimccntop  15396  limccnp2lem  15402  limccnp2cntop  15403  dvfvalap  15407  dvmptfsum  15451  dveflem  15452  plyco  15485  plycn  15488  plyrecj  15489  reeff1olem  15497  reeff1oleme  15498  eflt  15501  sin0pilem2  15508  pilem3  15509  ptolemy  15550  ioocosf1o  15580  cxplt  15642  cxple  15643  cxplt3  15646  apcxp2  15665  rprelogbmul  15681  rprelogbdiv  15683  logbgt0b  15692  logbgcd1irrap  15696  fsumdvdsmul  15717  perfectlem2  15726  lgsdir2lem5  15763  lgsdir  15766  lgsdi  15768  lgsne0  15769  gausslemma2dlem1f1o  15791  lgseisenlem2  15802  lgsquadlem1  15808  lgsquadlem2  15809  lgsquad2lem2  15813  lgsquad2  15814  2sqlem6  15851  2sqlem10  15856  upgredg  15997  uhgrissubgr  16114  subgrprop3  16115  upgrspanop  16136  umgrspanop  16137  usgrspanop  16138  vtxedgfi  16142  vtxlpfi  16143  upgr2wlkdc  16230  clwwlkccatlem  16253  nnti  16594  pwtrufal  16601  pwf1oexmid  16603  sssneq  16606  qdencn  16634  cvgcmp2n  16640  trilpolemlt1  16648  trirec0  16651  trirec0xor  16652  redc0  16664  reap0  16665  cndcap  16666  nconstwlpolemgt0  16671  neap0mkv  16676  supfz  16678  inffz  16679  gfsumval  16683  gfsumcl  16690