Theorem simplll 485

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

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

Proof of Theorem simplll

Step	Hyp	Ref	Expression
1		simpl 102	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	ad2antrr 457	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> 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:  f1imass  5413  tfrlem1  5923  phplem4dom  6324  phplem4on  6329  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  ltexnqq  6506  enq0tr  6532  addcmpblnq0  6541  mulcmpblnq0  6542  nnnq0lem1  6544  prssnql  6577  prmuloc  6664  prmuloc2  6665  mullocpr  6669  ltexprlemopu  6701  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  ltmprr  6740  archpr  6741  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  ltsrprg  6832  srpospr  6867  axcaucvglemres  6973  negeu  7202  add20  7469  rimul  7576  apreap  7578  cru  7593  mulge0  7610  mulap0  7635  prodgt0  7818  ltmul12a  7826  ledivdiv  7856  lediv12a  7860  qapne  8574  qreccl  8576  ixxss12  8775  ioodisj  8861  fznlem  8905  elfz0fzfz0  8983  btwnzge0  9142  mulexpzap  9295  leexp1a  9309  expnbnd  9372  resqrexlemga  9621  sqrtsq  9642  abs3lem  9707  cau3lem  9710  climcau  9866