Theorem simpll 481

Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)

Assertion

Ref	Expression
simpll	|- ( ( ( ph /\ ps ) /\ ch ) -> ph )

Proof of Theorem simpll

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2	1	ad2antrr 457	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  simp1ll  967  simp2ll  971  simp3ll  975  rmob  2850  prneimg  3545  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  poinxp  4409  mpteqb  5261  fvmptt  5262  fcof1  5423  acexmid  5511  grprinvlem  5695  dftpos4  5878  tfrlem3ag  5924  tfrlem3a  5925  tfrlemi1  5946  tfrexlem  5948  nndifsnid  6080  qsel  6183  ecopovsymg  6205  ecopoverg  6207  th3qlem1  6208  fidifsnid  6332  findcard2  6346  findcard2s  6347  findcard2sd  6349  dfplpq2  6452  dfmpq2  6453  mulpipqqs  6471  distrnqg  6485  ltexnqq  6506  subhalfnqq  6512  prarloclemarch  6516  nnnq0lem1  6544  distrnq0  6557  npsspw  6569  prarloclemlo  6592  prarloclem3  6595  prarloclemcalc  6600  genplt2i  6608  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  ltprordil  6687  ltexprlemlol  6700  ltexprlemupu  6702  addextpr  6719  recexprlemopl  6723  recexprlemdisj  6728  recexprlem1ssl  6731  aptiprleml  6737  prsrlem1  6827  recexgt0sr  6858  addcnsr  6910  mulcnsr  6911  mulcnsrec  6919  axaddcl  6940  axmulcl  6942  axmulcom  6945  rereceu  6963  cnegexlem1  7186  cnegex  7189  addsub4  7254  le2add  7439  lt2add  7440  lt2sub  7455  le2sub  7456  rereim  7577  apreim  7594  mulreim  7595  addext  7601  mulext  7605  receuap  7650  rec11ap  7686  rec11rap  7687  divdivdivap  7689  ddcanap  7702  divadddivap  7703  divsubdivap  7704  conjmulap  7705  rerecclap  7706  recgt0  7816  prodgt0gt0  7817  prodgt0  7818  prodge0  7820  ltmul12a  7826  lemul12a  7828  lemulge11  7832  lt2mul2div  7845  ltrec  7849  lerec  7850  lt2msq  7852  ltrec1  7854  le2msq  7867  msq11  7868  ledivp1  7869  peano5uzti  8346  eluzuzle  8481  qreccl  8576  xrltso  8717  z2ge  8739  ixxss1  8773  ixxss2  8774  elioc2  8805  divelunit  8870  fzass4  8925  fzrev  8946  fzonmapblen  9043  elfzodifsumelfzo  9057  ssfzo12bi  9081  qbtwnzlemstep  9103  qbtwnzlemex  9105  rebtwn2z  9109  expivallem  9256  expp1  9262  expcl2lemap  9267  expnegzap  9289  expadd  9297  expmul  9300  leexp1a  9309  expnlbnd  9373  shftfvalg  9419  shftfval  9422  caucvgrelemrec  9578  resqrexlemdecn  9610  sqrtmul  9633  sqrtdiv  9640  leabs  9672  absexpzap  9676  ltabs  9683  abslt  9684  absle  9685  abssubap0  9686  amgm2  9714  icodiamlt  9776  qdenre  9798  climuni  9814  cn1lem  9834  iiserex  9859  iserile  9862  climcau  9866  sqrt2irr  9878  qdencn  10124