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  3122  elpr2elpr  3853  disjiun  4077  reg3exmidlemwe  4670  0xp  4798  imainss  5143  iotam  5309  fvmptt  5725  fcof1o  5912  isotr  5939  riota5f  5980  ovmpodf  6135  unielxp  6318  fnmpoovd  6359  1stconst  6365  2ndconst  6366  cnvf1olem  6368  tfrlemi14d  6477  tfrexlem  6478  tfr1onlemres  6493  tfrcllemres  6506  tfrcldm  6507  frecabcl  6543  nnaordi  6652  swoer  6706  qliftfun  6762  ecopovsymg  6779  th3qlem1  6782  pw2f1odclem  6991  mapen  7003  mapxpen  7005  fidifsnen  7028  fisbth  7041  findcard2d  7049  findcard2sd  7050  diffisn  7051  diffifi  7052  ac6sfi  7056  fimax2gtri  7059  fientri3  7073  nnwetri  7074  unsnfi  7077  unsnfidcex  7078  unsnfidcel  7079  fisseneq  7092  fidcenumlemrk  7117  fidcenumlemr  7118  isbth  7130  ordiso2  7198  difinfsnlem  7262  difinfinf  7264  ctmlemr  7271  ctssdccl  7274  fodjum  7309  fodju0  7310  omniwomnimkv  7330  exmidfodomrlemrALT  7377  netap  7436  exmidmotap  7443  cc1  7447  cc2lem  7448  cc3  7450  cc4f  7451  cc4n  7453  dfplpq2  7537  dfmpq2  7538  mulpipqqs  7556  distrnqg  7570  ltexnqq  7591  subhalfnqq  7597  distrnq0  7642  prarloclemup  7678  prarloclem3  7680  prarloc  7686  genplt2i  7693  nqprl  7734  nqpru  7735  prmuloc  7749  mullocpr  7754  distrlem4prl  7767  distrlem4pru  7768  ltaddpr  7780  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemrl  7793  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  ltaprlem  7801  ltaprg  7802  prplnqu  7803  addextpr  7804  recexprlemdisj  7813  recexprlemloc  7814  recexprlem1ssl  7816  aptiprleml  7822  aptiprlemu  7823  ltmprr  7825  archpr  7826  cauappcvgprlemopl  7829  cauappcvgprlemopu  7831  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlem1  7842  cauappcvgprlem2  7843  cauappcvgprlemlim  7844  caucvgprlemnkj  7849  caucvgprlemopl  7852  caucvgprlemopu  7854  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlem2  7863  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemnjltk  7874  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemopu  7882  caucvgprprlemdisj  7885  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  caucvgprprlemaddq  7891  caucvgprprlem2  7893  suplocexprlemrl  7900  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemex  7905  suplocexprlemub  7906  suplocexprlemlub  7907  recexgt0sr  7956  mulgt0sr  7961  prsrriota  7971  caucvgsrlemoffres  7983  suplocsrlem  7991  cnm  8015  addcnsr  8017  mulcnsr  8018  mulcnsrec  8026  axaddcl  8047  axmulcl  8049  axmulcom  8054  rereceu  8072  recriota  8073  axcaucvglemres  8082  axpre-suploclemres  8084  lelttr  8231  ltletr  8232  readdcan  8282  addcan  8322  addcan2  8323  addsub4  8385  ltadd2  8562  le2add  8587  lt2add  8588  lt2sub  8603  le2sub  8604  eqord1  8626  rimul  8728  rereim  8729  ltmul1  8735  apreim  8746  mulreim  8747  apcotr  8750  apadd1  8751  addext  8753  apneg  8754  mulext1  8755  mulext  8757  ltleap  8775  aprcl  8789  mulap0  8797  mulcanapd  8804  receuap  8812  recapb  8814  rec11ap  8853  rec11rap  8854  divdivdivap  8856  ddcanap  8869  divadddivap  8870  conjmulap  8872  subrecap  8982  prodgt0gt0  8994  prodge0  8997  ltmul12a  9003  lemulge11  9009  lt2mul2div  9022  ltrec  9026  lerec  9027  lt2msq  9029  lerec2  9032  le2msq  9044  msq11  9045  ledivp1  9046  mulle0r  9087  suprzclex  9541  peano5uzti  9551  supinfneg  9786  infsupneg  9787  qapne  9830  xrlelttr  9998  xrltletr  9999  xrre  10012  xaddge0  10070  xle2add  10071  xlt2add  10072  divelunit  10194  fzass4  10254  fzocatel  10400  zsupcllemstep  10444  zssinfcl  10447  suprzubdc  10451  zsupssdc  10453  suprzcl2dc  10454  exbtwnzlemex  10464  rebtwn2z  10469  qbtwnre  10471  modqid  10566  modqcyc  10576  modqaddabs  10579  modqaddmod  10580  mulqaddmodid  10581  modqadd2mod  10591  modqltm1p1mod  10593  modqsubmod  10599  modqsubmodmod  10600  modqmulmod  10606  modqmulmodr  10607  modqaddmulmod  10608  modqsubdir  10610  frec2uzisod  10624  iseqovex  10675  seqvalcd  10678  seq1g  10680  seqf  10681  seqovcd  10684  seqm1g  10691  seq3fveq2  10692  seq3shft2  10698  seqshft2g  10699  monoord  10702  seq3split  10705  seqsplitg  10706  iseqf1olemnab  10718  seqf1oglem1  10736  seqf1og  10738  seq3id2  10743  seqhomog  10747  seq3distr  10749  expcl2lemap  10768  expnegzap  10790  ltexp2a  10808  le2sq2  10832  nn0ltexp2  10926  nn0opth2  10941  bcval5  10980  hashcl  10998  hashen  11001  fihashdom  11020  hashunlem  11021  hashun  11022  fimaxq  11044  zfz1isolem1  11057  zfz1iso  11058  lencl  11070  sswrd  11075  fstwrdne0  11106  lswlgt0cl  11119  swrdval  11175  wrdind  11249  wrd2ind  11250  swrdccatfn  11251  swrdccatin1  11252  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12  11260  pfxccat3a  11265  reuccatpfxs1  11274  cvg1nlemres  11491  cvg1n  11492  recvguniq  11501  resqrexlemp1rp  11512  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemex  11531  sqrtmul  11541  sqrtsq  11550  absexpzap  11586  absle  11595  abs3lem  11617  amgm2  11624  maxleastlt  11721  maxltsup  11724  fimaxre2  11733  xrmaxleastlt  11762  xrmaxltsup  11764  xrmaxaddlem  11766  climcn2  11815  addcn2  11816  mulcn2  11818  reccn2ap  11819  climcau  11853  summodclem2  11888  summodc  11889  fsumf1o  11896  fisumss  11898  fsum3cvg3  11902  fsumcl2lem  11904  fsumadd  11912  fsum2dlemstep  11940  mptfzshft  11948  fsumrev  11949  fsummulc2  11954  modfsummod  11964  fsumrelem  11977  binom  11990  cvgratnn  12037  mertenslemub  12040  prodmodc  12084  zproddc  12085  fprodf1o  12094  fprodssdc  12096  fprodmul  12097  fprodrev  12125  fprod2dlemstep  12128  efcllem  12165  tanaddaplem  12244  dvdsval2  12296  moddvds  12305  dvdsabseq  12353  dvdsflip  12357  oexpneg  12383  fldivndvdslt  12443  bitsfi  12463  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemeu  12523  dfgcd3  12526  bezout  12527  dvdsmulgcd  12541  bezoutr  12548  nninfctlemfo  12556  ialgrlem1st  12559  lcmgcdlem  12594  coprmdvds2  12610  qredeu  12614  rpdvds  12616  isprm5lem  12658  isprm6  12664  pw2dvdslemn  12682  nonsq  12724  crth  12741  eulerthlemh  12748  pclemdc  12806  pcprendvds2  12809  pceu  12813  pcval  12814  pczpre  12815  pcmul  12819  pcqmul  12821  pcqcl  12824  pcid  12842  pcneg  12843  pcgcd1  12846  pc2dvds  12848  pcprmpw2  12851  difsqpwdvds  12856  pcmpt  12861  pockthg  12875  1arith  12885  mul4sq  12912  4sqexercise2  12917  ennnfonelemg  12969  ennnfonelemex  12980  ennnfonelemrnh  12982  ennnfonelemrn  12985  ennnfonelemdm  12986  ennnfonelemnn0  12988  ennnfonelemim  12990  ennnfone  12991  ctinfomlemom  12993  ctinf  12996  ctiunctlemfo  13005  nninfdclemcl  13014  nninfdclemf  13015  nninfdclemp1  13016  unbendc  13020  isstruct2r  13038  setscom  13067  qusval  13351  ercpbl  13359  opifismgmdc  13399  grpinvalem  13413  grprida  13415  igsumvalx  13417  gsumfzval  13419  gsumpropd2  13421  gsumval2  13425  sgrppropd  13441  prdssgrpd  13443  mndpropd  13468  issubmnd  13470  submnd0  13472  prdsmndd  13476  mhmf1o  13498  0mhm  13514  resmhm  13515  mhmco  13518  mhmima  13519  mhmeql  13520  gsumwsubmcl  13524  gsumfzcl  13527  grppropd  13545  grpinvid1  13580  grpinvid2  13581  grplcan  13590  grplmulf1o  13602  grpnpncan0  13624  dfgrp3mlem  13626  grplactcnv  13630  pwssub  13641  mulgval  13654  mulgfng  13656  mulg1  13661  mulgnnp1  13662  mulgneg  13672  mulgnndir  13683  mulgdirlem  13685  mulgnn0ass  13690  mulgass  13691  subgmulg  13720  issubg4m  13725  subgintm  13730  0nsg  13746  eqgcpbl  13760  ghmmulg  13788  ghmpreima  13798  ghmeql  13799  ghmnsgima  13800  ghmnsgpreima  13801  ghmf1  13805  ghmf1o  13807  conjghm  13808  conjnmzb  13812  qusghm  13814  ablpncan3  13849  invghm  13861  eqgabl  13862  qusecsub  13863  gsumfzreidx  13869  gsumfzsubmcl  13870  gsumfzmptfidmadd  13871  gsumfzmhm  13875  imasrng  13914  qusrng  13916  srglmhm  13951  srgrmhm  13952  ringpropd  13996  ringlghm  14019  ringrghm  14020  imasring  14022  qusring2  14024  opprrngbg  14036  dvdsrvald  14051  dvdsrd  14052  dvdsrex  14056  dvdsrtr  14059  unitgrp  14074  unitpropdg  14106  rhmopp  14134  isnzr2  14142  issubrng2  14168  subrngintm  14170  subrgintm  14201  rhmpropd  14212  aprap  14244  lmodprop2d  14306  rmodislmodlem  14308  lssvacl  14323  lssvsubcl  14324  lssvscl  14333  islss3  14337  lsspropdg  14389  rnglidlmcl  14438  2idlcpblrng  14481  crngridl  14488  expghmap  14565  mulgghm2  14566  mulgrhm  14567  znf1o  14609  znleval  14611  znidom  14615  psrval  14624  mplsubgfilemcl  14657  epttop  14758  topssnei  14830  restbasg  14836  restopnb  14849  cnfval  14862  cnpfval  14863  iscnp4  14886  cnpnei  14887  cnptopco  14890  cncnp  14898  cnrest2  14904  cnptoprest  14907  cnptoprest2  14908  lmss  14914  lmtopcnp  14918  neitx  14936  txcnp  14939  txrest  14944  txdis  14945  txlm  14947  cnmpt21  14959  imasnopn  14967  xmetres2  15047  blvalps  15056  blval  15057  bl2in  15071  blhalf  15076  blssps  15095  blss  15096  blssexps  15097  blssex  15098  ssblex  15099  blin2  15100  metss2lem  15165  bdmetval  15168  bdmopn  15172  metrest  15174  xmetxp  15175  xmetxpbl  15176  xmettx  15178  metcnp3  15179  txmetcnp  15186  addcncntoplem  15229  elcncf2  15242  mulc1cncf  15257  cncfco  15259  cncfmet  15260  mulcncf  15276  dedekindeulemub  15286  dedekindeulemloc  15287  dedekindeulemlu  15289  dedekindeu  15291  suplociccex  15293  dedekindicclemub  15295  dedekindicclemloc  15296  dedekindicclemlu  15298  dedekindicc  15301  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthdec  15312  ivthreinc  15313  dich0  15320  limcimolemlt  15332  limcimo  15333  cnplimccntop  15338  limccnp2lem  15344  limccnp2cntop  15345  dvfvalap  15349  dvmptfsum  15393  dveflem  15394  plyco  15427  plycn  15430  plyrecj  15431  reeff1olem  15439  reeff1oleme  15440  eflt  15443  sin0pilem2  15450  pilem3  15451  ptolemy  15492  ioocosf1o  15522  cxplt  15584  cxple  15585  cxplt3  15588  apcxp2  15607  rprelogbmul  15623  rprelogbdiv  15625  logbgt0b  15634  logbgcd1irrap  15638  fsumdvdsmul  15659  perfectlem2  15668  lgsdir2lem5  15705  lgsdir  15708  lgsdi  15710  lgsne0  15711  gausslemma2dlem1f1o  15733  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem2  15755  lgsquad2  15756  2sqlem6  15793  2sqlem10  15798  upgredg  15936  nnti  16315  pwtrufal  16322  pwf1oexmid  16324  sssneq  16327  qdencn  16354  cvgcmp2n  16360  trilpolemlt1  16368  trirec0  16371  trirec0xor  16372  redc0  16384  reap0  16385  cndcap  16386  nconstwlpolemgt0  16391  neap0mkv  16396  supfz  16398  inffz  16399