Theorem simplll 500

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 107	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	ad2antrr 472	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  simp-4l  508  f1imass  5493  tfrlem1  6005  phplem4dom  6508  phplem4on  6513  fisseneq  6567  suplub2ti  6603  addcmpblnq  6829  mulcmpblnq  6830  ordpipqqs  6836  ltexnqq  6870  enq0tr  6896  addcmpblnq0  6905  mulcmpblnq0  6906  nnnq0lem1  6908  prssnql  6941  prmuloc  7028  prmuloc2  7029  mullocpr  7033  ltexprlemopu  7065  ltexprlemrl  7072  ltexprlemru  7074  addcanprleml  7076  addcanprlemu  7077  ltmprr  7104  archpr  7105  addcmpblnr  7188  mulcmpblnrlemg  7189  mulcmpblnr  7190  ltsrprg  7196  srpospr  7231  axcaucvglemres  7337  negeu  7576  add20  7855  rimul  7962  apreap  7964  cru  7979  mulge0  7996  mulap0  8021  prodgt0  8207  ltmul12a  8215  ledivdiv  8245  lediv12a  8249  qapne  9019  qreccl  9022  ixxss12  9219  ioodisj  9305  fznlem  9350  elfz0fzfz0  9428  btwnzge0  9596  mulexpzap  9832  leexp1a  9847  expnbnd  9912  hashennnuni  10022  resqrexlemga  10283  sqrtsq  10304  abs3lem  10371  cau3lem  10374  minmax  10486  climcau  10558  dvdsle  10625  gcdsupex  10729  gcdsupcl  10730  bezoutlemmain  10767  bezoutlemzz  10771  dfgcd3  10779  dvdsmulgcd  10794  lcmcllem  10829  lcmgcdlem  10839  ncoprmgcdne1b  10851  qredeu  10859  oddpwdclemxy  10927  oddpwdclemdc  10931  nninfalllemn  11239  nninfalllem1  11240