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  3136  elpr2elpr  3880  disjiun  4104  reg3exmidlemwe  4701  opabssxpd  4786  0xp  4830  imainss  5178  iotam  5344  fvmptt  5769  fcof1o  5962  isotr  5989  riota5f  6030  ovmpodf  6185  unielxp  6368  fnmpoovd  6411  1stconst  6417  2ndconst  6418  cnvf1olem  6420  fvn0elsupp  6451  suppcofn  6466  tfrlemi14d  6564  tfrexlem  6565  tfr1onlemres  6580  tfrcllemres  6593  tfrcldm  6594  frecabcl  6630  nnaordi  6741  swoer  6795  qliftfun  6851  ecopovsymg  6868  th3qlem1  6871  pw2f1odclem  7087  mapen  7099  mapxpen  7101  fidifsnen  7125  fisbth  7140  findcard2d  7148  findcard2sd  7149  diffisn  7150  diffifi  7151  ac6sfi  7155  fidcen  7156  fimax2gtri  7159  fientri3  7175  nnwetri  7176  unsnfi  7179  unsnfidcex  7180  unsnfidcel  7181  fisseneq  7195  exmidssfi  7199  fidcenumlemrk  7224  fidcenumlemr  7225  isbth  7237  ordiso2  7326  difinfsnlem  7390  difinfinf  7392  ctmlemr  7399  ctssdccl  7402  fodjum  7437  fodju0  7438  omniwomnimkv  7458  exmidfodomrlemrALT  7506  netap  7568  exmidmotap  7575  cc1  7579  cc2lem  7580  cc3  7582  cc4f  7583  cc4n  7585  dfplpq2  7669  dfmpq2  7670  mulpipqqs  7688  distrnqg  7702  ltexnqq  7723  subhalfnqq  7729  distrnq0  7774  prarloclemup  7810  prarloclem3  7812  prarloc  7818  genplt2i  7825  nqprl  7866  nqpru  7867  prmuloc  7881  mullocpr  7886  distrlem4prl  7899  distrlem4pru  7900  ltaddpr  7912  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemrl  7925  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  ltaprlem  7933  ltaprg  7934  prplnqu  7935  addextpr  7936  recexprlemdisj  7945  recexprlemloc  7946  recexprlem1ssl  7948  aptiprleml  7954  aptiprlemu  7955  ltmprr  7957  archpr  7958  cauappcvgprlemopl  7961  cauappcvgprlemopu  7963  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlem1  7974  cauappcvgprlem2  7975  cauappcvgprlemlim  7976  caucvgprlemnkj  7981  caucvgprlemopl  7984  caucvgprlemopu  7986  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlem2  7995  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemnjltk  8006  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemopu  8014  caucvgprprlemdisj  8017  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  caucvgprprlemaddq  8023  caucvgprprlem2  8025  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemex  8037  suplocexprlemub  8038  suplocexprlemlub  8039  recexgt0sr  8088  mulgt0sr  8093  prsrriota  8103  caucvgsrlemoffres  8115  suplocsrlem  8123  cnm  8147  addcnsr  8149  mulcnsr  8150  mulcnsrec  8158  axaddcl  8179  axmulcl  8181  axmulcom  8186  rereceu  8204  recriota  8205  axcaucvglemres  8214  axpre-suploclemres  8216  lelttr  8362  ltletr  8363  readdcan  8413  addcan  8453  addcan2  8454  addsub4  8516  ltadd2  8693  le2add  8718  lt2add  8719  lt2sub  8734  le2sub  8735  eqord1  8757  rimul  8859  rereim  8860  ltmul1  8866  apreim  8877  mulreim  8878  apcotr  8881  apadd1  8882  addext  8884  apneg  8885  mulext1  8886  mulext  8888  ltleap  8906  aprcl  8920  mulap0  8928  mulcanapd  8935  receuap  8943  recapb  8945  rec11ap  8984  rec11rap  8985  divdivdivap  8987  ddcanap  9000  divadddivap  9001  conjmulap  9003  subrecap  9113  prodgt0gt0  9125  prodge0  9128  ltmul12a  9134  lemulge11  9140  lt2mul2div  9153  ltrec  9157  lerec  9158  lt2msq  9160  lerec2  9163  le2msq  9175  msq11  9176  ledivp1  9177  mulle0r  9218  suprzclex  9676  peano5uzti  9686  supinfneg  9927  infsupneg  9928  qapne  9971  xrlelttr  10139  xrltletr  10140  xrre  10153  xaddge0  10211  xle2add  10212  xlt2add  10213  divelunit  10335  fzass4  10396  fzocatel  10544  zsupcllemstep  10589  zssinfcl  10592  suprzubdc  10596  zsupssdc  10598  suprzcl2dc  10599  exbtwnzlemex  10609  rebtwn2z  10614  qbtwnre  10616  modqid  10711  modqcyc  10721  modqaddabs  10724  modqaddmod  10725  mulqaddmodid  10726  modqadd2mod  10736  modqltm1p1mod  10738  modqsubmod  10744  modqsubmodmod  10745  modqmulmod  10751  modqmulmodr  10752  modqaddmulmod  10753  modqsubdir  10755  frec2uzisod  10769  iseqovex  10820  seqvalcd  10823  seq1g  10825  seqf  10826  seqovcd  10829  seqm1g  10836  seq3fveq2  10837  seq3shft2  10843  seqshft2g  10844  monoord  10847  seq3split  10850  seqsplitg  10851  iseqf1olemnab  10863  seqf1oglem1  10881  seqf1og  10883  seq3id2  10888  seqhomog  10892  seq3distr  10894  expcl2lemap  10913  expnegzap  10935  ltexp2a  10953  le2sq2  10977  nn0ltexp2  11071  nn0opth2  11086  bcval5  11125  hashcl  11144  hashen  11147  fihashdom  11167  hashunlem  11168  hashun  11169  hashmap  11192  fimaxq  11194  hashfibclem  11206  hashfibc  11207  zfz1isolem1  11212  zfz1iso  11213  lencl  11228  sswrd  11233  fstwrdne0  11264  lswlgt0cl  11277  ccatw2s1p1g  11333  ccat2s1fstg  11336  swrdval  11340  wrdind  11414  wrd2ind  11415  swrdccatfn  11416  swrdccatin1  11417  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12  11425  pfxccat3a  11430  reuccatpfxs1  11439  cvg1nlemres  11670  cvg1n  11671  recvguniq  11680  resqrexlemp1rp  11691  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemex  11710  sqrtmul  11720  sqrtsq  11729  absexpzap  11765  absle  11774  abs3lem  11796  amgm2  11803  maxleastlt  11900  maxltsup  11903  fimaxre2  11912  xrmaxleastlt  11941  xrmaxltsup  11943  xrmaxaddlem  11945  climcn2  11994  addcn2  11995  mulcn2  11997  reccn2ap  11998  climcau  12032  summodclem2  12068  summodc  12069  fsumf1o  12076  fisumss  12078  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  fsum2dlemstep  12120  mptfzshft  12128  fsumrev  12129  fsummulc2  12134  modfsummod  12144  fsumrelem  12157  binom  12170  cvgratnn  12217  mertenslemub  12220  prodmodc  12264  zproddc  12265  fprodf1o  12274  fprodssdc  12276  fprodmul  12277  fprodrev  12305  fprod2dlemstep  12308  efcllem  12345  tanaddaplem  12424  dvdsval2  12476  moddvds  12485  dvdsabseq  12533  dvdsflip  12537  oexpneg  12563  fldivndvdslt  12623  bitsfi  12643  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemeu  12703  dfgcd3  12706  bezout  12707  dvdsmulgcd  12721  bezoutr  12728  nninfctlemfo  12736  ialgrlem1st  12739  lcmgcdlem  12774  coprmdvds2  12790  qredeu  12794  rpdvds  12796  isprm5lem  12838  isprm6  12844  pw2dvdslemn  12862  nonsq  12904  crth  12921  eulerthlemh  12928  pclemdc  12986  pcprendvds2  12989  pceu  12993  pcval  12994  pczpre  12995  pcmul  12999  pcqmul  13001  pcqcl  13004  pcid  13022  pcneg  13023  pcgcd1  13026  pc2dvds  13028  pcprmpw2  13031  difsqpwdvds  13036  pcmpt  13041  pockthg  13055  1arith  13065  mul4sq  13092  4sqexercise2  13097  ennnfonelemg  13154  ennnfonelemex  13165  ennnfonelemrnh  13167  ennnfonelemrn  13170  ennnfonelemdm  13171  ennnfonelemnn0  13173  ennnfonelemim  13175  ennnfone  13176  ctinfomlemom  13178  ctinf  13181  ctiunctlemfo  13190  nninfdclemcl  13199  nninfdclemf  13200  nninfdclemp1  13201  unbendc  13205  isstruct2r  13223  setscom  13252  qusval  13536  ercpbl  13544  opifismgmdc  13584  grpinvalem  13598  grprida  13600  igsumvalx  13602  gsumfzval  13604  gsumpropd2  13606  gsumval2  13610  sgrppropd  13626  prdssgrpd  13628  mndpropd  13653  issubmnd  13655  submnd0  13657  prdsmndd  13661  mhmf1o  13683  0mhm  13699  resmhm  13700  mhmco  13703  mhmima  13704  mhmeql  13705  gsumwsubmcl  13709  gsumfzcl  13712  grppropd  13730  grpinvid1  13765  grpinvid2  13766  grplcan  13775  grplmulf1o  13787  grpnpncan0  13809  dfgrp3mlem  13811  grplactcnv  13815  pwssub  13826  mulgval  13839  mulgfng  13841  mulg1  13846  mulgnnp1  13847  mulgneg  13857  mulgnndir  13868  mulgdirlem  13870  mulgnn0ass  13875  mulgass  13876  subgmulg  13905  issubg4m  13910  subgintm  13915  0nsg  13931  eqgcpbl  13945  ghmmulg  13973  ghmpreima  13983  ghmeql  13984  ghmnsgima  13985  ghmnsgpreima  13986  ghmf1  13990  ghmf1o  13992  conjghm  13993  conjnmzb  13997  qusghm  13999  ablpncan3  14034  invghm  14046  eqgabl  14047  qusecsub  14048  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  imasrng  14100  qusrng  14102  srglmhm  14137  srgrmhm  14138  ringpropd  14182  ringlghm  14205  ringrghm  14206  imasring  14208  qusring2  14210  opprrngbg  14222  dvdsrvald  14238  dvdsrd  14239  dvdsrex  14243  dvdsrtr  14246  unitgrp  14261  unitpropdg  14293  rhmopp  14321  isnzr2  14329  issubrng2  14355  subrngintm  14357  subrgintm  14388  rhmpropd  14399  aprap  14432  lmodprop2d  14496  rmodislmodlem  14498  lssvacl  14513  lssvsubcl  14514  lssvscl  14523  islss3  14527  lsspropdg  14579  rnglidlmcl  14628  2idlcpblrng  14671  crngridl  14678  expghmap  14755  mulgghm2  14756  mulgrhm  14757  znf1o  14799  znleval  14801  znidom  14805  psrval  14814  psrbagcon  14826  psrbagconf1o  14828  mplsubgfilemcl  14854  epttop  14955  topssnei  15027  restbasg  15033  restopnb  15046  cnfval  15059  cnpfval  15060  iscnp4  15083  cnpnei  15084  cnptopco  15087  cncnp  15095  cnrest2  15101  cnptoprest  15104  cnptoprest2  15105  lmss  15111  lmtopcnp  15115  neitx  15133  txcnp  15136  txrest  15141  txdis  15142  txlm  15144  cnmpt21  15156  imasnopn  15164  xmetres2  15244  blvalps  15253  blval  15254  bl2in  15268  blhalf  15273  blssps  15292  blss  15293  blssexps  15294  blssex  15295  ssblex  15296  blin2  15297  metss2lem  15362  bdmetval  15365  bdmopn  15369  metrest  15371  xmetxp  15372  xmetxpbl  15373  xmettx  15375  metcnp3  15376  txmetcnp  15383  addcncntoplem  15426  elcncf2  15439  mulc1cncf  15454  cncfco  15456  cncfmet  15457  mulcncf  15473  dedekindeulemub  15483  dedekindeulemloc  15484  dedekindeulemlu  15486  dedekindeu  15488  suplociccex  15490  dedekindicclemub  15492  dedekindicclemloc  15493  dedekindicclemlu  15495  dedekindicc  15498  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthdec  15509  ivthreinc  15510  dich0  15517  limcimolemlt  15529  limcimo  15530  cnplimccntop  15535  limccnp2lem  15541  limccnp2cntop  15542  dvfvalap  15546  dvmptfsum  15590  dveflem  15591  plyco  15624  plycn  15627  plyrecj  15628  reeff1olem  15636  reeff1oleme  15637  eflt  15640  sin0pilem2  15647  pilem3  15648  ptolemy  15689  ioocosf1o  15719  cxplt  15781  cxple  15782  cxplt3  15785  apcxp2  15804  rprelogbmul  15820  rprelogbdiv  15822  logbgt0b  15831  logbgcd1irrap  15835  pellexlem3  15847  fsumdvdsmul  15859  perfectlem2  15868  lgsdir2lem5  15905  lgsdir  15908  lgsdi  15910  lgsne0  15911  gausslemma2dlem1f1o  15933  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  lgsquad2  15956  2sqlem6  15993  2sqlem10  15998  upgredg  16139  uhgrissubgr  16256  subgrprop3  16257  upgrspanop  16278  umgrspanop  16279  usgrspanop  16280  vtxedgfi  16284  vtxlpfi  16285  upgr2wlkdc  16372  clwwlkccatlem  16395  eupth2lemsfi  16473  depindlem3  16503  nnti  16766  pwtrufal  16771  pwf1oexmid  16773  sssneq  16776  qdencn  16807  cvgcmp2n  16817  trilpolemlt1  16825  trirec0  16828  trirec0xor  16829  qdiff  16833  redc0  16842  reap0  16843  cndcap  16844  trimul0or  16845  nconstwlpolemgt0  16850  neap0mkv  16855  supfz  16857  inffz  16858  gfsumval  16862  gfsumcl  16870