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  3126  elpr2elpr  3864  disjiun  4088  reg3exmidlemwe  4683  opabssxpd  4768  0xp  4812  imainss  5159  iotam  5325  fvmptt  5747  fcof1o  5940  isotr  5967  riota5f  6008  ovmpodf  6163  unielxp  6346  fnmpoovd  6389  1stconst  6395  2ndconst  6396  cnvf1olem  6398  fvn0elsupp  6429  suppcofn  6444  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemres  6558  tfrcllemres  6571  tfrcldm  6572  frecabcl  6608  nnaordi  6719  swoer  6773  qliftfun  6829  ecopovsymg  6846  th3qlem1  6849  pw2f1odclem  7063  mapen  7075  mapxpen  7077  fidifsnen  7100  fisbth  7115  findcard2d  7123  findcard2sd  7124  diffisn  7125  diffifi  7126  ac6sfi  7130  fidcen  7131  fimax2gtri  7134  fientri3  7150  nnwetri  7151  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  fisseneq  7170  exmidssfi  7174  fidcenumlemrk  7196  fidcenumlemr  7197  isbth  7209  ordiso2  7277  difinfsnlem  7341  difinfinf  7343  ctmlemr  7350  ctssdccl  7353  fodjum  7388  fodju0  7389  omniwomnimkv  7409  exmidfodomrlemrALT  7457  netap  7516  exmidmotap  7523  cc1  7527  cc2lem  7528  cc3  7530  cc4f  7531  cc4n  7533  dfplpq2  7617  dfmpq2  7618  mulpipqqs  7636  distrnqg  7650  ltexnqq  7671  subhalfnqq  7677  distrnq0  7722  prarloclemup  7758  prarloclem3  7760  prarloc  7766  genplt2i  7773  nqprl  7814  nqpru  7815  prmuloc  7829  mullocpr  7834  distrlem4prl  7847  distrlem4pru  7848  ltaddpr  7860  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  ltaprlem  7881  ltaprg  7882  prplnqu  7883  addextpr  7884  recexprlemdisj  7893  recexprlemloc  7894  recexprlem1ssl  7896  aptiprleml  7902  aptiprlemu  7903  ltmprr  7905  archpr  7906  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlem1  7922  cauappcvgprlem2  7923  cauappcvgprlemlim  7924  caucvgprlemnkj  7929  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlem2  7943  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemnjltk  7954  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemopu  7962  caucvgprprlemdisj  7965  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  caucvgprprlemaddq  7971  caucvgprprlem2  7973  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemex  7985  suplocexprlemub  7986  suplocexprlemlub  7987  recexgt0sr  8036  mulgt0sr  8041  prsrriota  8051  caucvgsrlemoffres  8063  suplocsrlem  8071  cnm  8095  addcnsr  8097  mulcnsr  8098  mulcnsrec  8106  axaddcl  8127  axmulcl  8129  axmulcom  8134  rereceu  8152  recriota  8153  axcaucvglemres  8162  axpre-suploclemres  8164  lelttr  8310  ltletr  8311  readdcan  8361  addcan  8401  addcan2  8402  addsub4  8464  ltadd2  8641  le2add  8666  lt2add  8667  lt2sub  8682  le2sub  8683  eqord1  8705  rimul  8807  rereim  8808  ltmul1  8814  apreim  8825  mulreim  8826  apcotr  8829  apadd1  8830  addext  8832  apneg  8833  mulext1  8834  mulext  8836  ltleap  8854  aprcl  8868  mulap0  8876  mulcanapd  8883  receuap  8891  recapb  8893  rec11ap  8932  rec11rap  8933  divdivdivap  8935  ddcanap  8948  divadddivap  8949  conjmulap  8951  subrecap  9061  prodgt0gt0  9073  prodge0  9076  ltmul12a  9082  lemulge11  9088  lt2mul2div  9101  ltrec  9105  lerec  9106  lt2msq  9108  lerec2  9111  le2msq  9123  msq11  9124  ledivp1  9125  mulle0r  9166  suprzclex  9622  peano5uzti  9632  supinfneg  9873  infsupneg  9874  qapne  9917  xrlelttr  10085  xrltletr  10086  xrre  10099  xaddge0  10157  xle2add  10158  xlt2add  10159  divelunit  10281  fzass4  10342  fzocatel  10490  zsupcllemstep  10535  zssinfcl  10538  suprzubdc  10542  zsupssdc  10544  suprzcl2dc  10545  exbtwnzlemex  10555  rebtwn2z  10560  qbtwnre  10562  modqid  10657  modqcyc  10667  modqaddabs  10670  modqaddmod  10671  mulqaddmodid  10672  modqadd2mod  10682  modqltm1p1mod  10684  modqsubmod  10690  modqsubmodmod  10691  modqmulmod  10697  modqmulmodr  10698  modqaddmulmod  10699  modqsubdir  10701  frec2uzisod  10715  iseqovex  10766  seqvalcd  10769  seq1g  10771  seqf  10772  seqovcd  10775  seqm1g  10782  seq3fveq2  10783  seq3shft2  10789  seqshft2g  10790  monoord  10793  seq3split  10796  seqsplitg  10797  iseqf1olemnab  10809  seqf1oglem1  10827  seqf1og  10829  seq3id2  10834  seqhomog  10838  seq3distr  10840  expcl2lemap  10859  expnegzap  10881  ltexp2a  10899  le2sq2  10923  nn0ltexp2  11017  nn0opth2  11032  bcval5  11071  hashcl  11089  hashen  11092  fihashdom  11112  hashunlem  11113  hashun  11114  fimaxq  11137  zfz1isolem1  11150  zfz1iso  11151  lencl  11166  sswrd  11171  fstwrdne0  11202  lswlgt0cl  11215  ccatw2s1p1g  11271  ccat2s1fstg  11274  swrdval  11278  wrdind  11352  wrd2ind  11353  swrdccatfn  11354  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12  11363  pfxccat3a  11368  reuccatpfxs1  11377  cvg1nlemres  11608  cvg1n  11609  recvguniq  11618  resqrexlemp1rp  11629  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemex  11648  sqrtmul  11658  sqrtsq  11667  absexpzap  11703  absle  11712  abs3lem  11734  amgm2  11741  maxleastlt  11838  maxltsup  11841  fimaxre2  11850  xrmaxleastlt  11879  xrmaxltsup  11881  xrmaxaddlem  11883  climcn2  11932  addcn2  11933  mulcn2  11935  reccn2ap  11936  climcau  11970  summodclem2  12006  summodc  12007  fsumf1o  12014  fisumss  12016  fsum3cvg3  12020  fsumcl2lem  12022  fsumadd  12030  fsum2dlemstep  12058  mptfzshft  12066  fsumrev  12067  fsummulc2  12072  modfsummod  12082  fsumrelem  12095  binom  12108  cvgratnn  12155  mertenslemub  12158  prodmodc  12202  zproddc  12203  fprodf1o  12212  fprodssdc  12214  fprodmul  12215  fprodrev  12243  fprod2dlemstep  12246  efcllem  12283  tanaddaplem  12362  dvdsval2  12414  moddvds  12423  dvdsabseq  12471  dvdsflip  12475  oexpneg  12501  fldivndvdslt  12561  bitsfi  12581  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemeu  12641  dfgcd3  12644  bezout  12645  dvdsmulgcd  12659  bezoutr  12666  nninfctlemfo  12674  ialgrlem1st  12677  lcmgcdlem  12712  coprmdvds2  12728  qredeu  12732  rpdvds  12734  isprm5lem  12776  isprm6  12782  pw2dvdslemn  12800  nonsq  12842  crth  12859  eulerthlemh  12866  pclemdc  12924  pcprendvds2  12927  pceu  12931  pcval  12932  pczpre  12933  pcmul  12937  pcqmul  12939  pcqcl  12942  pcid  12960  pcneg  12961  pcgcd1  12964  pc2dvds  12966  pcprmpw2  12969  difsqpwdvds  12974  pcmpt  12979  pockthg  12993  1arith  13003  mul4sq  13030  4sqexercise2  13035  ennnfonelemg  13087  ennnfonelemex  13098  ennnfonelemrnh  13100  ennnfonelemrn  13103  ennnfonelemdm  13104  ennnfonelemnn0  13106  ennnfonelemim  13108  ennnfone  13109  ctinfomlemom  13111  ctinf  13114  ctiunctlemfo  13123  nninfdclemcl  13132  nninfdclemf  13133  nninfdclemp1  13134  unbendc  13138  isstruct2r  13156  setscom  13185  qusval  13469  ercpbl  13477  opifismgmdc  13517  grpinvalem  13531  grprida  13533  igsumvalx  13535  gsumfzval  13537  gsumpropd2  13539  gsumval2  13543  sgrppropd  13559  prdssgrpd  13561  mndpropd  13586  issubmnd  13588  submnd0  13590  prdsmndd  13594  mhmf1o  13616  0mhm  13632  resmhm  13633  mhmco  13636  mhmima  13637  mhmeql  13638  gsumwsubmcl  13642  gsumfzcl  13645  grppropd  13663  grpinvid1  13698  grpinvid2  13699  grplcan  13708  grplmulf1o  13720  grpnpncan0  13742  dfgrp3mlem  13744  grplactcnv  13748  pwssub  13759  mulgval  13772  mulgfng  13774  mulg1  13779  mulgnnp1  13780  mulgneg  13790  mulgnndir  13801  mulgdirlem  13803  mulgnn0ass  13808  mulgass  13809  subgmulg  13838  issubg4m  13843  subgintm  13848  0nsg  13864  eqgcpbl  13878  ghmmulg  13906  ghmpreima  13916  ghmeql  13917  ghmnsgima  13918  ghmnsgpreima  13919  ghmf1  13923  ghmf1o  13925  conjghm  13926  conjnmzb  13930  qusghm  13932  ablpncan3  13967  invghm  13979  eqgabl  13980  qusecsub  13981  gsumfzreidx  13987  gsumfzsubmcl  13988  gsumfzmptfidmadd  13989  gsumfzmhm  13993  imasrng  14033  qusrng  14035  srglmhm  14070  srgrmhm  14071  ringpropd  14115  ringlghm  14138  ringrghm  14139  imasring  14141  qusring2  14143  opprrngbg  14155  dvdsrvald  14171  dvdsrd  14172  dvdsrex  14176  dvdsrtr  14179  unitgrp  14194  unitpropdg  14226  rhmopp  14254  isnzr2  14262  issubrng2  14288  subrngintm  14290  subrgintm  14321  rhmpropd  14332  aprap  14365  lmodprop2d  14427  rmodislmodlem  14429  lssvacl  14444  lssvsubcl  14445  lssvscl  14454  islss3  14458  lsspropdg  14510  rnglidlmcl  14559  2idlcpblrng  14602  crngridl  14609  expghmap  14686  mulgghm2  14687  mulgrhm  14688  znf1o  14730  znleval  14732  znidom  14736  psrval  14745  psrbagcon  14755  psrbagconf1o  14757  mplsubgfilemcl  14783  epttop  14884  topssnei  14956  restbasg  14962  restopnb  14975  cnfval  14988  cnpfval  14989  iscnp4  15012  cnpnei  15013  cnptopco  15016  cncnp  15024  cnrest2  15030  cnptoprest  15033  cnptoprest2  15034  lmss  15040  lmtopcnp  15044  neitx  15062  txcnp  15065  txrest  15070  txdis  15071  txlm  15073  cnmpt21  15085  imasnopn  15093  xmetres2  15173  blvalps  15182  blval  15183  bl2in  15197  blhalf  15202  blssps  15221  blss  15222  blssexps  15223  blssex  15224  ssblex  15225  blin2  15226  metss2lem  15291  bdmetval  15294  bdmopn  15298  metrest  15300  xmetxp  15301  xmetxpbl  15302  xmettx  15304  metcnp3  15305  txmetcnp  15312  addcncntoplem  15355  elcncf2  15368  mulc1cncf  15383  cncfco  15385  cncfmet  15386  mulcncf  15402  dedekindeulemub  15412  dedekindeulemloc  15413  dedekindeulemlu  15415  dedekindeu  15417  suplociccex  15419  dedekindicclemub  15421  dedekindicclemloc  15422  dedekindicclemlu  15424  dedekindicc  15427  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthdec  15438  ivthreinc  15439  dich0  15446  limcimolemlt  15458  limcimo  15459  cnplimccntop  15464  limccnp2lem  15470  limccnp2cntop  15471  dvfvalap  15475  dvmptfsum  15519  dveflem  15520  plyco  15553  plycn  15556  plyrecj  15557  reeff1olem  15565  reeff1oleme  15566  eflt  15569  sin0pilem2  15576  pilem3  15577  ptolemy  15618  ioocosf1o  15648  cxplt  15710  cxple  15711  cxplt3  15714  apcxp2  15733  rprelogbmul  15749  rprelogbdiv  15751  logbgt0b  15760  logbgcd1irrap  15764  pellexlem3  15776  fsumdvdsmul  15788  perfectlem2  15797  lgsdir2lem5  15834  lgsdir  15837  lgsdi  15839  lgsne0  15840  gausslemma2dlem1f1o  15862  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem2  15884  lgsquad2  15885  2sqlem6  15922  2sqlem10  15927  upgredg  16068  uhgrissubgr  16185  subgrprop3  16186  upgrspanop  16207  umgrspanop  16208  usgrspanop  16209  vtxedgfi  16213  vtxlpfi  16214  upgr2wlkdc  16301  clwwlkccatlem  16324  eupth2lemsfi  16402  depindlem3  16432  nnti  16695  pwtrufal  16702  pwf1oexmid  16704  sssneq  16707  qdencn  16738  cvgcmp2n  16748  trilpolemlt1  16756  trirec0  16759  trirec0xor  16760  qdiff  16764  redc0  16773  reap0  16774  cndcap  16775  nconstwlpolemgt0  16780  neap0mkv  16785  supfz  16787  inffz  16788  gfsumval  16792  gfsumcl  16799