Theorem simplll 503

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simp-4l  511  f1imass  5607  tfrlem1  6135  phplem4dom  6685  phplem4on  6690  fisseneq  6749  suplub2ti  6803  omp1eomlem  6894  addcmpblnq  7076  mulcmpblnq  7077  ordpipqqs  7083  ltexnqq  7117  enq0tr  7143  addcmpblnq0  7152  mulcmpblnq0  7153  nnnq0lem1  7155  prssnql  7188  prmuloc  7275  prmuloc2  7276  mullocpr  7280  ltexprlemopu  7312  ltexprlemrl  7319  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  ltmprr  7351  archpr  7352  addcmpblnr  7435  mulcmpblnrlemg  7436  mulcmpblnr  7437  ltsrprg  7443  srpospr  7478  axcaucvglemres  7584  negeu  7824  add20  8103  rimul  8213  apreap  8215  cru  8230  mulge0  8247  mulap0  8276  prodgt0  8468  ltmul12a  8476  ledivdiv  8506  lediv12a  8510  qapne  9281  qreccl  9284  xleaddadd  9511  ixxss12  9530  ioodisj  9617  fznlem  9662  elfz0fzfz0  9744  btwnzge0  9914  mulexpzap  10174  leexp1a  10189  expnbnd  10256  hashennnuni  10366  zfz1iso  10425  seq3coll  10426  resqrexlemga  10635  sqrtsq  10656  abs3lem  10723  cau3lem  10726  minmax  10840  xrmaxiflemval  10858  xrminmax  10873  climcau  10955  summodclem2  10990  fsumrelem  11079  cvgratz  11140  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  dvdsle  11337  gcdsupex  11441  gcdsupcl  11442  bezoutlemmain  11479  bezoutlemzz  11483  dfgcd3  11491  dvdsmulgcd  11506  lcmcllem  11541  lcmgcdlem  11551  ncoprmgcdne1b  11563  qredeu  11571  oddpwdclemxy  11639  oddpwdclemdc  11643  neissex  12116  restbasg  12119  tgrest  12120  restopnb  12132  cnptopco  12172  metequiv2  12424  metcnpi3  12441  elcncf2  12474  cncfmet  12492  limccnpcntop  12520  nninfalllemn  12786  nninfalllem1  12787