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  5535  tfrlem1  6055  phplem4dom  6558  phplem4on  6563  fisseneq  6621  suplub2ti  6675  addcmpblnq  6905  mulcmpblnq  6906  ordpipqqs  6912  ltexnqq  6946  enq0tr  6972  addcmpblnq0  6981  mulcmpblnq0  6982  nnnq0lem1  6984  prssnql  7017  prmuloc  7104  prmuloc2  7105  mullocpr  7109  ltexprlemopu  7141  ltexprlemrl  7148  ltexprlemru  7150  addcanprleml  7152  addcanprlemu  7153  ltmprr  7180  archpr  7181  addcmpblnr  7264  mulcmpblnrlemg  7265  mulcmpblnr  7266  ltsrprg  7272  srpospr  7307  axcaucvglemres  7413  negeu  7652  add20  7931  rimul  8038  apreap  8040  cru  8055  mulge0  8072  mulap0  8097  prodgt0  8285  ltmul12a  8293  ledivdiv  8323  lediv12a  8327  qapne  9093  qreccl  9096  ixxss12  9293  ioodisj  9379  fznlem  9424  elfz0fzfz0  9502  btwnzge0  9672  mulexpzap  9959  leexp1a  9974  expnbnd  10041  hashennnuni  10151  zfz1iso  10210  iseqcoll  10211  resqrexlemga  10420  sqrtsq  10441  abs3lem  10508  cau3lem  10511  minmax  10624  climcau  10699  isummolem2  10734  fsumrelem  10826  dvdsle  10925  gcdsupex  11029  gcdsupcl  11030  bezoutlemmain  11067  bezoutlemzz  11071  dfgcd3  11079  dvdsmulgcd  11094  lcmcllem  11129  lcmgcdlem  11139  ncoprmgcdne1b  11151  qredeu  11159  oddpwdclemxy  11227  oddpwdclemdc  11231  nninfalllemn  11542  nninfalllem1  11543