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  989  simp1rl  1088  simp2rl  1092  simp3rl  1096  rmob  3125  elpr2elpr  3859  disjiun  4083  reg3exmidlemwe  4677  opabssxpd  4762  0xp  4806  imainss  5152  iotam  5318  fvmptt  5738  fcof1o  5929  isotr  5956  riota5f  5997  ovmpodf  6152  unielxp  6336  fnmpoovd  6379  1stconst  6385  2ndconst  6386  cnvf1olem  6388  tfrlemi14d  6498  tfrexlem  6499  tfr1onlemres  6514  tfrcllemres  6527  tfrcldm  6528  frecabcl  6564  nnaordi  6675  swoer  6729  qliftfun  6785  ecopovsymg  6802  th3qlem1  6805  pw2f1odclem  7019  mapen  7031  mapxpen  7033  fidifsnen  7056  fisbth  7071  findcard2d  7079  findcard2sd  7080  diffisn  7081  diffifi  7082  ac6sfi  7086  fidcen  7087  fimax2gtri  7090  fientri3  7106  nnwetri  7107  unsnfi  7110  unsnfidcex  7111  unsnfidcel  7112  fisseneq  7126  exmidssfi  7130  fidcenumlemrk  7152  fidcenumlemr  7153  isbth  7165  ordiso2  7233  difinfsnlem  7297  difinfinf  7299  ctmlemr  7306  ctssdccl  7309  fodjum  7344  fodju0  7345  omniwomnimkv  7365  exmidfodomrlemrALT  7413  netap  7472  exmidmotap  7479  cc1  7483  cc2lem  7484  cc3  7486  cc4f  7487  cc4n  7489  dfplpq2  7573  dfmpq2  7574  mulpipqqs  7592  distrnqg  7606  ltexnqq  7627  subhalfnqq  7633  distrnq0  7678  prarloclemup  7714  prarloclem3  7716  prarloc  7722  genplt2i  7729  nqprl  7770  nqpru  7771  prmuloc  7785  mullocpr  7790  distrlem4prl  7803  distrlem4pru  7804  ltaddpr  7816  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemrl  7829  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  ltaprlem  7837  ltaprg  7838  prplnqu  7839  addextpr  7840  recexprlemdisj  7849  recexprlemloc  7850  recexprlem1ssl  7852  aptiprleml  7858  aptiprlemu  7859  ltmprr  7861  archpr  7862  cauappcvgprlemopl  7865  cauappcvgprlemopu  7867  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlem1  7878  cauappcvgprlem2  7879  cauappcvgprlemlim  7880  caucvgprlemnkj  7885  caucvgprlemopl  7888  caucvgprlemopu  7890  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlem2  7899  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnjltk  7910  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemopu  7918  caucvgprprlemdisj  7921  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  caucvgprprlemaddq  7927  caucvgprprlem2  7929  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemex  7941  suplocexprlemub  7942  suplocexprlemlub  7943  recexgt0sr  7992  mulgt0sr  7997  prsrriota  8007  caucvgsrlemoffres  8019  suplocsrlem  8027  cnm  8051  addcnsr  8053  mulcnsr  8054  mulcnsrec  8062  axaddcl  8083  axmulcl  8085  axmulcom  8090  rereceu  8108  recriota  8109  axcaucvglemres  8118  axpre-suploclemres  8120  lelttr  8267  ltletr  8268  readdcan  8318  addcan  8358  addcan2  8359  addsub4  8421  ltadd2  8598  le2add  8623  lt2add  8624  lt2sub  8639  le2sub  8640  eqord1  8662  rimul  8764  rereim  8765  ltmul1  8771  apreim  8782  mulreim  8783  apcotr  8786  apadd1  8787  addext  8789  apneg  8790  mulext1  8791  mulext  8793  ltleap  8811  aprcl  8825  mulap0  8833  mulcanapd  8840  receuap  8848  recapb  8850  rec11ap  8889  rec11rap  8890  divdivdivap  8892  ddcanap  8905  divadddivap  8906  conjmulap  8908  subrecap  9018  prodgt0gt0  9030  prodge0  9033  ltmul12a  9039  lemulge11  9045  lt2mul2div  9058  ltrec  9062  lerec  9063  lt2msq  9065  lerec2  9068  le2msq  9080  msq11  9081  ledivp1  9082  mulle0r  9123  suprzclex  9577  peano5uzti  9587  supinfneg  9828  infsupneg  9829  qapne  9872  xrlelttr  10040  xrltletr  10041  xrre  10054  xaddge0  10112  xle2add  10113  xlt2add  10114  divelunit  10236  fzass4  10296  fzocatel  10443  zsupcllemstep  10488  zssinfcl  10491  suprzubdc  10495  zsupssdc  10497  suprzcl2dc  10498  exbtwnzlemex  10508  rebtwn2z  10513  qbtwnre  10515  modqid  10610  modqcyc  10620  modqaddabs  10623  modqaddmod  10624  mulqaddmodid  10625  modqadd2mod  10635  modqltm1p1mod  10637  modqsubmod  10643  modqsubmodmod  10644  modqmulmod  10650  modqmulmodr  10651  modqaddmulmod  10652  modqsubdir  10654  frec2uzisod  10668  iseqovex  10719  seqvalcd  10722  seq1g  10724  seqf  10725  seqovcd  10728  seqm1g  10735  seq3fveq2  10736  seq3shft2  10742  seqshft2g  10743  monoord  10746  seq3split  10749  seqsplitg  10750  iseqf1olemnab  10762  seqf1oglem1  10780  seqf1og  10782  seq3id2  10787  seqhomog  10791  seq3distr  10793  expcl2lemap  10812  expnegzap  10834  ltexp2a  10852  le2sq2  10876  nn0ltexp2  10970  nn0opth2  10985  bcval5  11024  hashcl  11042  hashen  11045  fihashdom  11065  hashunlem  11066  hashun  11067  fimaxq  11090  zfz1isolem1  11103  zfz1iso  11104  lencl  11116  sswrd  11121  fstwrdne0  11152  lswlgt0cl  11165  ccatw2s1p1g  11221  ccat2s1fstg  11224  swrdval  11228  wrdind  11302  wrd2ind  11303  swrdccatfn  11304  swrdccatin1  11305  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  pfxccat3a  11318  reuccatpfxs1  11327  cvg1nlemres  11545  cvg1n  11546  recvguniq  11555  resqrexlemp1rp  11566  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemex  11585  sqrtmul  11595  sqrtsq  11604  absexpzap  11640  absle  11649  abs3lem  11671  amgm2  11678  maxleastlt  11775  maxltsup  11778  fimaxre2  11787  xrmaxleastlt  11816  xrmaxltsup  11818  xrmaxaddlem  11820  climcn2  11869  addcn2  11870  mulcn2  11872  reccn2ap  11873  climcau  11907  summodclem2  11942  summodc  11943  fsumf1o  11950  fisumss  11952  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  fsum2dlemstep  11994  mptfzshft  12002  fsumrev  12003  fsummulc2  12008  modfsummod  12018  fsumrelem  12031  binom  12044  cvgratnn  12091  mertenslemub  12094  prodmodc  12138  zproddc  12139  fprodf1o  12148  fprodssdc  12150  fprodmul  12151  fprodrev  12179  fprod2dlemstep  12182  efcllem  12219  tanaddaplem  12298  dvdsval2  12350  moddvds  12359  dvdsabseq  12407  dvdsflip  12411  oexpneg  12437  fldivndvdslt  12497  bitsfi  12517  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemeu  12577  dfgcd3  12580  bezout  12581  dvdsmulgcd  12595  bezoutr  12602  nninfctlemfo  12610  ialgrlem1st  12613  lcmgcdlem  12648  coprmdvds2  12664  qredeu  12668  rpdvds  12670  isprm5lem  12712  isprm6  12718  pw2dvdslemn  12736  nonsq  12778  crth  12795  eulerthlemh  12802  pclemdc  12860  pcprendvds2  12863  pceu  12867  pcval  12868  pczpre  12869  pcmul  12873  pcqmul  12875  pcqcl  12878  pcid  12896  pcneg  12897  pcgcd1  12900  pc2dvds  12902  pcprmpw2  12905  difsqpwdvds  12910  pcmpt  12915  pockthg  12929  1arith  12939  mul4sq  12966  4sqexercise2  12971  ennnfonelemg  13023  ennnfonelemex  13034  ennnfonelemrnh  13036  ennnfonelemrn  13039  ennnfonelemdm  13040  ennnfonelemnn0  13042  ennnfonelemim  13044  ennnfone  13045  ctinfomlemom  13047  ctinf  13050  ctiunctlemfo  13059  nninfdclemcl  13068  nninfdclemf  13069  nninfdclemp1  13070  unbendc  13074  isstruct2r  13092  setscom  13121  qusval  13405  ercpbl  13413  opifismgmdc  13453  grpinvalem  13467  grprida  13469  igsumvalx  13471  gsumfzval  13473  gsumpropd2  13475  gsumval2  13479  sgrppropd  13495  prdssgrpd  13497  mndpropd  13522  issubmnd  13524  submnd0  13526  prdsmndd  13530  mhmf1o  13552  0mhm  13568  resmhm  13569  mhmco  13572  mhmima  13573  mhmeql  13574  gsumwsubmcl  13578  gsumfzcl  13581  grppropd  13599  grpinvid1  13634  grpinvid2  13635  grplcan  13644  grplmulf1o  13656  grpnpncan0  13678  dfgrp3mlem  13680  grplactcnv  13684  pwssub  13695  mulgval  13708  mulgfng  13710  mulg1  13715  mulgnnp1  13716  mulgneg  13726  mulgnndir  13737  mulgdirlem  13739  mulgnn0ass  13744  mulgass  13745  subgmulg  13774  issubg4m  13779  subgintm  13784  0nsg  13800  eqgcpbl  13814  ghmmulg  13842  ghmpreima  13852  ghmeql  13853  ghmnsgima  13854  ghmnsgpreima  13855  ghmf1  13859  ghmf1o  13861  conjghm  13862  conjnmzb  13866  qusghm  13868  ablpncan3  13903  invghm  13915  eqgabl  13916  qusecsub  13917  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  imasrng  13968  qusrng  13970  srglmhm  14005  srgrmhm  14006  ringpropd  14050  ringlghm  14073  ringrghm  14074  imasring  14076  qusring2  14078  opprrngbg  14090  dvdsrvald  14106  dvdsrd  14107  dvdsrex  14111  dvdsrtr  14114  unitgrp  14129  unitpropdg  14161  rhmopp  14189  isnzr2  14197  issubrng2  14223  subrngintm  14225  subrgintm  14256  rhmpropd  14267  aprap  14299  lmodprop2d  14361  rmodislmodlem  14363  lssvacl  14378  lssvsubcl  14379  lssvscl  14388  islss3  14392  lsspropdg  14444  rnglidlmcl  14493  2idlcpblrng  14536  crngridl  14543  expghmap  14620  mulgghm2  14621  mulgrhm  14622  znf1o  14664  znleval  14666  znidom  14670  psrval  14679  mplsubgfilemcl  14712  epttop  14813  topssnei  14885  restbasg  14891  restopnb  14904  cnfval  14917  cnpfval  14918  iscnp4  14941  cnpnei  14942  cnptopco  14945  cncnp  14953  cnrest2  14959  cnptoprest  14962  cnptoprest2  14963  lmss  14969  lmtopcnp  14973  neitx  14991  txcnp  14994  txrest  14999  txdis  15000  txlm  15002  cnmpt21  15014  imasnopn  15022  xmetres2  15102  blvalps  15111  blval  15112  bl2in  15126  blhalf  15131  blssps  15150  blss  15151  blssexps  15152  blssex  15153  ssblex  15154  blin2  15155  metss2lem  15220  bdmetval  15223  bdmopn  15227  metrest  15229  xmetxp  15230  xmetxpbl  15231  xmettx  15233  metcnp3  15234  txmetcnp  15241  addcncntoplem  15284  elcncf2  15297  mulc1cncf  15312  cncfco  15314  cncfmet  15315  mulcncf  15331  dedekindeulemub  15341  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeu  15346  suplociccex  15348  dedekindicclemub  15350  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthdec  15367  ivthreinc  15368  dich0  15375  limcimolemlt  15387  limcimo  15388  cnplimccntop  15393  limccnp2lem  15399  limccnp2cntop  15400  dvfvalap  15404  dvmptfsum  15448  dveflem  15449  plyco  15482  plycn  15485  plyrecj  15486  reeff1olem  15494  reeff1oleme  15495  eflt  15498  sin0pilem2  15505  pilem3  15506  ptolemy  15547  ioocosf1o  15577  cxplt  15639  cxple  15640  cxplt3  15643  apcxp2  15662  rprelogbmul  15678  rprelogbdiv  15680  logbgt0b  15689  logbgcd1irrap  15693  fsumdvdsmul  15714  perfectlem2  15723  lgsdir2lem5  15760  lgsdir  15763  lgsdi  15765  lgsne0  15766  gausslemma2dlem1f1o  15788  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  lgsquad2  15811  2sqlem6  15848  2sqlem10  15853  upgredg  15994  uhgrissubgr  16111  subgrprop3  16112  upgrspanop  16133  umgrspanop  16134  usgrspanop  16135  vtxedgfi  16139  vtxlpfi  16140  upgr2wlkdc  16227  clwwlkccatlem  16250  nnti  16591  pwtrufal  16598  pwf1oexmid  16600  sssneq  16603  qdencn  16631  cvgcmp2n  16637  trilpolemlt1  16645  trirec0  16648  trirec0xor  16649  redc0  16661  reap0  16662  cndcap  16663  nconstwlpolemgt0  16668  neap0mkv  16673  supfz  16675  inffz  16676  gfsumval  16680