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:  dfifp2dc  987  simp1rl  1086  simp2rl  1090  simp3rl  1094  rmob  3123  elpr2elpr  3857  disjiun  4081  reg3exmidlemwe  4675  opabssxpd  4760  0xp  4804  imainss  5150  iotam  5316  fvmptt  5734  fcof1o  5925  isotr  5952  riota5f  5993  ovmpodf  6148  unielxp  6332  fnmpoovd  6375  1stconst  6381  2ndconst  6382  cnvf1olem  6384  tfrlemi14d  6494  tfrexlem  6495  tfr1onlemres  6510  tfrcllemres  6523  tfrcldm  6524  frecabcl  6560  nnaordi  6671  swoer  6725  qliftfun  6781  ecopovsymg  6798  th3qlem1  6801  pw2f1odclem  7015  mapen  7027  mapxpen  7029  fidifsnen  7052  fisbth  7065  findcard2d  7073  findcard2sd  7074  diffisn  7075  diffifi  7076  ac6sfi  7080  fidcen  7081  fimax2gtri  7084  fientri3  7100  nnwetri  7101  unsnfi  7104  unsnfidcex  7105  unsnfidcel  7106  fisseneq  7119  fidcenumlemrk  7144  fidcenumlemr  7145  isbth  7157  ordiso2  7225  difinfsnlem  7289  difinfinf  7291  ctmlemr  7298  ctssdccl  7301  fodjum  7336  fodju0  7337  omniwomnimkv  7357  exmidfodomrlemrALT  7404  netap  7463  exmidmotap  7470  cc1  7474  cc2lem  7475  cc3  7477  cc4f  7478  cc4n  7480  dfplpq2  7564  dfmpq2  7565  mulpipqqs  7583  distrnqg  7597  ltexnqq  7618  subhalfnqq  7624  distrnq0  7669  prarloclemup  7705  prarloclem3  7707  prarloc  7713  genplt2i  7720  nqprl  7761  nqpru  7762  prmuloc  7776  mullocpr  7781  distrlem4prl  7794  distrlem4pru  7795  ltaddpr  7807  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemrl  7820  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  ltaprlem  7828  ltaprg  7829  prplnqu  7830  addextpr  7831  recexprlemdisj  7840  recexprlemloc  7841  recexprlem1ssl  7843  aptiprleml  7849  aptiprlemu  7850  ltmprr  7852  archpr  7853  cauappcvgprlemopl  7856  cauappcvgprlemopu  7858  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlem1  7869  cauappcvgprlem2  7870  cauappcvgprlemlim  7871  caucvgprlemnkj  7876  caucvgprlemopl  7879  caucvgprlemopu  7881  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlem2  7890  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemnjltk  7901  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemopu  7909  caucvgprprlemdisj  7912  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  caucvgprprlemaddq  7918  caucvgprprlem2  7920  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemex  7932  suplocexprlemub  7933  suplocexprlemlub  7934  recexgt0sr  7983  mulgt0sr  7988  prsrriota  7998  caucvgsrlemoffres  8010  suplocsrlem  8018  cnm  8042  addcnsr  8044  mulcnsr  8045  mulcnsrec  8053  axaddcl  8074  axmulcl  8076  axmulcom  8081  rereceu  8099  recriota  8100  axcaucvglemres  8109  axpre-suploclemres  8111  lelttr  8258  ltletr  8259  readdcan  8309  addcan  8349  addcan2  8350  addsub4  8412  ltadd2  8589  le2add  8614  lt2add  8615  lt2sub  8630  le2sub  8631  eqord1  8653  rimul  8755  rereim  8756  ltmul1  8762  apreim  8773  mulreim  8774  apcotr  8777  apadd1  8778  addext  8780  apneg  8781  mulext1  8782  mulext  8784  ltleap  8802  aprcl  8816  mulap0  8824  mulcanapd  8831  receuap  8839  recapb  8841  rec11ap  8880  rec11rap  8881  divdivdivap  8883  ddcanap  8896  divadddivap  8897  conjmulap  8899  subrecap  9009  prodgt0gt0  9021  prodge0  9024  ltmul12a  9030  lemulge11  9036  lt2mul2div  9049  ltrec  9053  lerec  9054  lt2msq  9056  lerec2  9059  le2msq  9071  msq11  9072  ledivp1  9073  mulle0r  9114  suprzclex  9568  peano5uzti  9578  supinfneg  9819  infsupneg  9820  qapne  9863  xrlelttr  10031  xrltletr  10032  xrre  10045  xaddge0  10103  xle2add  10104  xlt2add  10105  divelunit  10227  fzass4  10287  fzocatel  10434  zsupcllemstep  10479  zssinfcl  10482  suprzubdc  10486  zsupssdc  10488  suprzcl2dc  10489  exbtwnzlemex  10499  rebtwn2z  10504  qbtwnre  10506  modqid  10601  modqcyc  10611  modqaddabs  10614  modqaddmod  10615  mulqaddmodid  10616  modqadd2mod  10626  modqltm1p1mod  10628  modqsubmod  10634  modqsubmodmod  10635  modqmulmod  10641  modqmulmodr  10642  modqaddmulmod  10643  modqsubdir  10645  frec2uzisod  10659  iseqovex  10710  seqvalcd  10713  seq1g  10715  seqf  10716  seqovcd  10719  seqm1g  10726  seq3fveq2  10727  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  iseqf1olemnab  10753  seqf1oglem1  10771  seqf1og  10773  seq3id2  10778  seqhomog  10782  seq3distr  10784  expcl2lemap  10803  expnegzap  10825  ltexp2a  10843  le2sq2  10867  nn0ltexp2  10961  nn0opth2  10976  bcval5  11015  hashcl  11033  hashen  11036  fihashdom  11056  hashunlem  11057  hashun  11058  fimaxq  11081  zfz1isolem1  11094  zfz1iso  11095  lencl  11107  sswrd  11112  fstwrdne0  11143  lswlgt0cl  11156  ccatw2s1p1g  11212  ccat2s1fstg  11215  swrdval  11219  wrdind  11293  wrd2ind  11294  swrdccatfn  11295  swrdccatin1  11296  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12  11304  pfxccat3a  11309  reuccatpfxs1  11318  cvg1nlemres  11536  cvg1n  11537  recvguniq  11546  resqrexlemp1rp  11557  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemex  11576  sqrtmul  11586  sqrtsq  11595  absexpzap  11631  absle  11640  abs3lem  11662  amgm2  11669  maxleastlt  11766  maxltsup  11769  fimaxre2  11778  xrmaxleastlt  11807  xrmaxltsup  11809  xrmaxaddlem  11811  climcn2  11860  addcn2  11861  mulcn2  11863  reccn2ap  11864  climcau  11898  summodclem2  11933  summodc  11934  fsumf1o  11941  fisumss  11943  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  fsum2dlemstep  11985  mptfzshft  11993  fsumrev  11994  fsummulc2  11999  modfsummod  12009  fsumrelem  12022  binom  12035  cvgratnn  12082  mertenslemub  12085  prodmodc  12129  zproddc  12130  fprodf1o  12139  fprodssdc  12141  fprodmul  12142  fprodrev  12170  fprod2dlemstep  12173  efcllem  12210  tanaddaplem  12289  dvdsval2  12341  moddvds  12350  dvdsabseq  12398  dvdsflip  12402  oexpneg  12428  fldivndvdslt  12488  bitsfi  12508  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemeu  12568  dfgcd3  12571  bezout  12572  dvdsmulgcd  12586  bezoutr  12593  nninfctlemfo  12601  ialgrlem1st  12604  lcmgcdlem  12639  coprmdvds2  12655  qredeu  12659  rpdvds  12661  isprm5lem  12703  isprm6  12709  pw2dvdslemn  12727  nonsq  12769  crth  12786  eulerthlemh  12793  pclemdc  12851  pcprendvds2  12854  pceu  12858  pcval  12859  pczpre  12860  pcmul  12864  pcqmul  12866  pcqcl  12869  pcid  12887  pcneg  12888  pcgcd1  12891  pc2dvds  12893  pcprmpw2  12896  difsqpwdvds  12901  pcmpt  12906  pockthg  12920  1arith  12930  mul4sq  12957  4sqexercise2  12962  ennnfonelemg  13014  ennnfonelemex  13025  ennnfonelemrnh  13027  ennnfonelemrn  13030  ennnfonelemdm  13031  ennnfonelemnn0  13033  ennnfonelemim  13035  ennnfone  13036  ctinfomlemom  13038  ctinf  13041  ctiunctlemfo  13050  nninfdclemcl  13059  nninfdclemf  13060  nninfdclemp1  13061  unbendc  13065  isstruct2r  13083  setscom  13112  qusval  13396  ercpbl  13404  opifismgmdc  13444  grpinvalem  13458  grprida  13460  igsumvalx  13462  gsumfzval  13464  gsumpropd2  13466  gsumval2  13470  sgrppropd  13486  prdssgrpd  13488  mndpropd  13513  issubmnd  13515  submnd0  13517  prdsmndd  13521  mhmf1o  13543  0mhm  13559  resmhm  13560  mhmco  13563  mhmima  13564  mhmeql  13565  gsumwsubmcl  13569  gsumfzcl  13572  grppropd  13590  grpinvid1  13625  grpinvid2  13626  grplcan  13635  grplmulf1o  13647  grpnpncan0  13669  dfgrp3mlem  13671  grplactcnv  13675  pwssub  13686  mulgval  13699  mulgfng  13701  mulg1  13706  mulgnnp1  13707  mulgneg  13717  mulgnndir  13728  mulgdirlem  13730  mulgnn0ass  13735  mulgass  13736  subgmulg  13765  issubg4m  13770  subgintm  13775  0nsg  13791  eqgcpbl  13805  ghmmulg  13833  ghmpreima  13843  ghmeql  13844  ghmnsgima  13845  ghmnsgpreima  13846  ghmf1  13850  ghmf1o  13852  conjghm  13853  conjnmzb  13857  qusghm  13859  ablpncan3  13894  invghm  13906  eqgabl  13907  qusecsub  13908  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  imasrng  13959  qusrng  13961  srglmhm  13996  srgrmhm  13997  ringpropd  14041  ringlghm  14064  ringrghm  14065  imasring  14067  qusring2  14069  opprrngbg  14081  dvdsrvald  14097  dvdsrd  14098  dvdsrex  14102  dvdsrtr  14105  unitgrp  14120  unitpropdg  14152  rhmopp  14180  isnzr2  14188  issubrng2  14214  subrngintm  14216  subrgintm  14247  rhmpropd  14258  aprap  14290  lmodprop2d  14352  rmodislmodlem  14354  lssvacl  14369  lssvsubcl  14370  lssvscl  14379  islss3  14383  lsspropdg  14435  rnglidlmcl  14484  2idlcpblrng  14527  crngridl  14534  expghmap  14611  mulgghm2  14612  mulgrhm  14613  znf1o  14655  znleval  14657  znidom  14661  psrval  14670  mplsubgfilemcl  14703  epttop  14804  topssnei  14876  restbasg  14882  restopnb  14895  cnfval  14908  cnpfval  14909  iscnp4  14932  cnpnei  14933  cnptopco  14936  cncnp  14944  cnrest2  14950  cnptoprest  14953  cnptoprest2  14954  lmss  14960  lmtopcnp  14964  neitx  14982  txcnp  14985  txrest  14990  txdis  14991  txlm  14993  cnmpt21  15005  imasnopn  15013  xmetres2  15093  blvalps  15102  blval  15103  bl2in  15117  blhalf  15122  blssps  15141  blss  15142  blssexps  15143  blssex  15144  ssblex  15145  blin2  15146  metss2lem  15211  bdmetval  15214  bdmopn  15218  metrest  15220  xmetxp  15221  xmetxpbl  15222  xmettx  15224  metcnp3  15225  txmetcnp  15232  addcncntoplem  15275  elcncf2  15288  mulc1cncf  15303  cncfco  15305  cncfmet  15306  mulcncf  15322  dedekindeulemub  15332  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeu  15337  suplociccex  15339  dedekindicclemub  15341  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthdec  15358  ivthreinc  15359  dich0  15366  limcimolemlt  15378  limcimo  15379  cnplimccntop  15384  limccnp2lem  15390  limccnp2cntop  15391  dvfvalap  15395  dvmptfsum  15439  dveflem  15440  plyco  15473  plycn  15476  plyrecj  15477  reeff1olem  15485  reeff1oleme  15486  eflt  15489  sin0pilem2  15496  pilem3  15497  ptolemy  15538  ioocosf1o  15568  cxplt  15630  cxple  15631  cxplt3  15634  apcxp2  15653  rprelogbmul  15669  rprelogbdiv  15671  logbgt0b  15680  logbgcd1irrap  15684  fsumdvdsmul  15705  perfectlem2  15714  lgsdir2lem5  15751  lgsdir  15754  lgsdi  15756  lgsne0  15757  gausslemma2dlem1f1o  15779  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  lgsquad2  15802  2sqlem6  15839  2sqlem10  15844  upgredg  15983  vtxedgfi  16095  vtxlpfi  16096  upgr2wlkdc  16172  clwwlkccatlem  16195  nnti  16527  pwtrufal  16534  pwf1oexmid  16536  sssneq  16539  qdencn  16567  cvgcmp2n  16573  trilpolemlt1  16581  trirec0  16584  trirec0xor  16585  redc0  16597  reap0  16598  cndcap  16599  nconstwlpolemgt0  16604  neap0mkv  16609  supfz  16611  inffz  16612