Theorem simprl 529

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:  simp1rl  1064  simp2rl  1068  simp3rl  1072  rmob  3082  disjiun  4029  reg3exmidlemwe  4616  0xp  4744  imainss  5086  iotam  5251  fvmptt  5656  fcof1o  5839  isotr  5866  riota5f  5905  ovmpodf  6058  unielxp  6241  fnmpoovd  6282  1stconst  6288  2ndconst  6289  cnvf1olem  6291  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemres  6416  tfrcllemres  6429  tfrcldm  6430  frecabcl  6466  nnaordi  6575  swoer  6629  qliftfun  6685  ecopovsymg  6702  th3qlem1  6705  pw2f1odclem  6904  mapen  6916  mapxpen  6918  fidifsnen  6940  fisbth  6953  findcard2d  6961  findcard2sd  6962  diffisn  6963  diffifi  6964  ac6sfi  6968  fimax2gtri  6971  fientri3  6985  nnwetri  6986  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fisseneq  7004  fidcenumlemrk  7029  fidcenumlemr  7030  isbth  7042  ordiso2  7110  difinfsnlem  7174  difinfinf  7176  ctmlemr  7183  ctssdccl  7186  fodjum  7221  fodju0  7222  omniwomnimkv  7242  exmidfodomrlemrALT  7282  netap  7337  exmidmotap  7344  cc1  7348  cc2lem  7349  cc3  7351  cc4f  7352  cc4n  7354  dfplpq2  7438  dfmpq2  7439  mulpipqqs  7457  distrnqg  7471  ltexnqq  7492  subhalfnqq  7498  distrnq0  7543  prarloclemup  7579  prarloclem3  7581  prarloc  7587  genplt2i  7594  nqprl  7635  nqpru  7636  prmuloc  7650  mullocpr  7655  distrlem4prl  7668  distrlem4pru  7669  ltaddpr  7681  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  ltaprlem  7702  ltaprg  7703  prplnqu  7704  addextpr  7705  recexprlemdisj  7714  recexprlemloc  7715  recexprlem1ssl  7717  aptiprleml  7723  aptiprlemu  7724  ltmprr  7726  archpr  7727  cauappcvgprlemopl  7730  cauappcvgprlemopu  7732  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlem1  7743  cauappcvgprlem2  7744  cauappcvgprlemlim  7745  caucvgprlemnkj  7750  caucvgprlemopl  7753  caucvgprlemopu  7755  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlem2  7764  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemnjltk  7775  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemopu  7783  caucvgprprlemdisj  7786  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  caucvgprprlemaddq  7792  caucvgprprlem2  7794  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemex  7806  suplocexprlemub  7807  suplocexprlemlub  7808  recexgt0sr  7857  mulgt0sr  7862  prsrriota  7872  caucvgsrlemoffres  7884  suplocsrlem  7892  cnm  7916  addcnsr  7918  mulcnsr  7919  mulcnsrec  7927  axaddcl  7948  axmulcl  7950  axmulcom  7955  rereceu  7973  recriota  7974  axcaucvglemres  7983  axpre-suploclemres  7985  lelttr  8132  ltletr  8133  readdcan  8183  addcan  8223  addcan2  8224  addsub4  8286  ltadd2  8463  le2add  8488  lt2add  8489  lt2sub  8504  le2sub  8505  eqord1  8527  rimul  8629  rereim  8630  ltmul1  8636  apreim  8647  mulreim  8648  apcotr  8651  apadd1  8652  addext  8654  apneg  8655  mulext1  8656  mulext  8658  ltleap  8676  aprcl  8690  mulap0  8698  mulcanapd  8705  receuap  8713  recapb  8715  rec11ap  8754  rec11rap  8755  divdivdivap  8757  ddcanap  8770  divadddivap  8771  conjmulap  8773  subrecap  8883  prodgt0gt0  8895  prodge0  8898  ltmul12a  8904  lemulge11  8910  lt2mul2div  8923  ltrec  8927  lerec  8928  lt2msq  8930  lerec2  8933  le2msq  8945  msq11  8946  ledivp1  8947  mulle0r  8988  suprzclex  9441  peano5uzti  9451  supinfneg  9686  infsupneg  9687  qapne  9730  xrlelttr  9898  xrltletr  9899  xrre  9912  xaddge0  9970  xle2add  9971  xlt2add  9972  divelunit  10094  fzass4  10154  fzocatel  10292  zsupcllemstep  10336  zssinfcl  10339  suprzubdc  10343  zsupssdc  10345  suprzcl2dc  10346  exbtwnzlemex  10356  rebtwn2z  10361  qbtwnre  10363  modqid  10458  modqcyc  10468  modqaddabs  10471  modqaddmod  10472  mulqaddmodid  10473  modqadd2mod  10483  modqltm1p1mod  10485  modqsubmod  10491  modqsubmodmod  10492  modqmulmod  10498  modqmulmodr  10499  modqaddmulmod  10500  modqsubdir  10502  frec2uzisod  10516  iseqovex  10567  seqvalcd  10570  seq1g  10572  seqf  10573  seqovcd  10576  seqm1g  10583  seq3fveq2  10584  seq3shft2  10590  seqshft2g  10591  monoord  10594  seq3split  10597  seqsplitg  10598  iseqf1olemnab  10610  seqf1oglem1  10628  seqf1og  10630  seq3id2  10635  seqhomog  10639  seq3distr  10641  expcl2lemap  10660  expnegzap  10682  ltexp2a  10700  le2sq2  10724  nn0ltexp2  10818  nn0opth2  10833  bcval5  10872  hashcl  10890  hashen  10893  fihashdom  10912  hashunlem  10913  hashun  10914  fimaxq  10936  zfz1isolem1  10949  zfz1iso  10950  lencl  10956  sswrd  10961  fstwrdne0  10991  cvg1nlemres  11167  cvg1n  11168  recvguniq  11177  resqrexlemp1rp  11188  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemex  11207  sqrtmul  11217  sqrtsq  11226  absexpzap  11262  absle  11271  abs3lem  11293  amgm2  11300  maxleastlt  11397  maxltsup  11400  fimaxre2  11409  xrmaxleastlt  11438  xrmaxltsup  11440  xrmaxaddlem  11442  climcn2  11491  addcn2  11492  mulcn2  11494  reccn2ap  11495  climcau  11529  summodclem2  11564  summodc  11565  fsumf1o  11572  fisumss  11574  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  fsum2dlemstep  11616  mptfzshft  11624  fsumrev  11625  fsummulc2  11630  modfsummod  11640  fsumrelem  11653  binom  11666  cvgratnn  11713  mertenslemub  11716  prodmodc  11760  zproddc  11761  fprodf1o  11770  fprodssdc  11772  fprodmul  11773  fprodrev  11801  fprod2dlemstep  11804  efcllem  11841  tanaddaplem  11920  dvdsval2  11972  moddvds  11981  dvdsabseq  12029  dvdsflip  12033  oexpneg  12059  fldivndvdslt  12119  bitsfi  12139  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemeu  12199  dfgcd3  12202  bezout  12203  dvdsmulgcd  12217  bezoutr  12224  nninfctlemfo  12232  ialgrlem1st  12235  lcmgcdlem  12270  coprmdvds2  12286  qredeu  12290  rpdvds  12292  isprm5lem  12334  isprm6  12340  pw2dvdslemn  12358  nonsq  12400  crth  12417  eulerthlemh  12424  pclemdc  12482  pcprendvds2  12485  pceu  12489  pcval  12490  pczpre  12491  pcmul  12495  pcqmul  12497  pcqcl  12500  pcid  12518  pcneg  12519  pcgcd1  12522  pc2dvds  12524  pcprmpw2  12527  difsqpwdvds  12532  pcmpt  12537  pockthg  12551  1arith  12561  mul4sq  12588  4sqexercise2  12593  ennnfonelemg  12645  ennnfonelemex  12656  ennnfonelemrnh  12658  ennnfonelemrn  12661  ennnfonelemdm  12662  ennnfonelemnn0  12664  ennnfonelemim  12666  ennnfone  12667  ctinfomlemom  12669  ctinf  12672  ctiunctlemfo  12681  nninfdclemcl  12690  nninfdclemf  12691  nninfdclemp1  12692  unbendc  12696  isstruct2r  12714  setscom  12743  qusval  13025  ercpbl  13033  opifismgmdc  13073  grpinvalem  13087  grprida  13089  igsumvalx  13091  gsumfzval  13093  gsumpropd2  13095  gsumval2  13099  sgrppropd  13115  prdssgrpd  13117  mndpropd  13142  issubmnd  13144  submnd0  13146  prdsmndd  13150  mhmf1o  13172  0mhm  13188  resmhm  13189  mhmco  13192  mhmima  13193  mhmeql  13194  gsumwsubmcl  13198  gsumfzcl  13201  grppropd  13219  grpinvid1  13254  grpinvid2  13255  grplcan  13264  grplmulf1o  13276  grpnpncan0  13298  dfgrp3mlem  13300  grplactcnv  13304  pwssub  13315  mulgval  13328  mulgfng  13330  mulg1  13335  mulgnnp1  13336  mulgneg  13346  mulgnndir  13357  mulgdirlem  13359  mulgnn0ass  13364  mulgass  13365  subgmulg  13394  issubg4m  13399  subgintm  13404  0nsg  13420  eqgcpbl  13434  ghmmulg  13462  ghmpreima  13472  ghmeql  13473  ghmnsgima  13474  ghmnsgpreima  13475  ghmf1  13479  ghmf1o  13481  conjghm  13482  conjnmzb  13486  qusghm  13488  ablpncan3  13523  invghm  13535  eqgabl  13536  qusecsub  13537  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  imasrng  13588  qusrng  13590  srglmhm  13625  srgrmhm  13626  ringpropd  13670  ringlghm  13693  ringrghm  13694  imasring  13696  qusring2  13698  opprrngbg  13710  dvdsrvald  13725  dvdsrd  13726  dvdsrex  13730  dvdsrtr  13733  unitgrp  13748  unitpropdg  13780  rhmopp  13808  isnzr2  13816  issubrng2  13842  subrngintm  13844  subrgintm  13875  rhmpropd  13886  aprap  13918  lmodprop2d  13980  rmodislmodlem  13982  lssvacl  13997  lssvsubcl  13998  lssvscl  14007  islss3  14011  lsspropdg  14063  rnglidlmcl  14112  2idlcpblrng  14155  crngridl  14162  expghmap  14239  mulgghm2  14240  mulgrhm  14241  znf1o  14283  znleval  14285  znidom  14289  psrval  14296  epttop  14410  topssnei  14482  restbasg  14488  restopnb  14501  cnfval  14514  cnpfval  14515  iscnp4  14538  cnpnei  14539  cnptopco  14542  cncnp  14550  cnrest2  14556  cnptoprest  14559  cnptoprest2  14560  lmss  14566  lmtopcnp  14570  neitx  14588  txcnp  14591  txrest  14596  txdis  14597  txlm  14599  cnmpt21  14611  imasnopn  14619  xmetres2  14699  blvalps  14708  blval  14709  bl2in  14723  blhalf  14728  blssps  14747  blss  14748  blssexps  14749  blssex  14750  ssblex  14751  blin2  14752  metss2lem  14817  bdmetval  14820  bdmopn  14824  metrest  14826  xmetxp  14827  xmetxpbl  14828  xmettx  14830  metcnp3  14831  txmetcnp  14838  addcncntoplem  14881  elcncf2  14894  mulc1cncf  14909  cncfco  14911  cncfmet  14912  mulcncf  14928  dedekindeulemub  14938  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeu  14943  suplociccex  14945  dedekindicclemub  14947  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthdec  14964  ivthreinc  14965  dich0  14972  limcimolemlt  14984  limcimo  14985  cnplimccntop  14990  limccnp2lem  14996  limccnp2cntop  14997  dvfvalap  15001  dvmptfsum  15045  dveflem  15046  plyco  15079  plycn  15082  plyrecj  15083  reeff1olem  15091  reeff1oleme  15092  eflt  15095  sin0pilem2  15102  pilem3  15103  ptolemy  15144  ioocosf1o  15174  cxplt  15236  cxple  15237  cxplt3  15240  apcxp2  15259  rprelogbmul  15275  rprelogbdiv  15277  logbgt0b  15286  logbgcd1irrap  15290  fsumdvdsmul  15311  perfectlem2  15320  lgsdir2lem5  15357  lgsdir  15360  lgsdi  15362  lgsne0  15363  gausslemma2dlem1f1o  15385  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  lgsquad2  15408  2sqlem6  15445  2sqlem10  15450  nnti  15723  pwtrufal  15728  pwf1oexmid  15730  sssneq  15733  qdencn  15758  cvgcmp2n  15764  trilpolemlt1  15772  trirec0  15775  trirec0xor  15776  redc0  15788  reap0  15789  cndcap  15790  nconstwlpolemgt0  15795  neap0mkv  15800  supfz  15802  inffz  15803