Theorem simplll 528

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 485	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simp-4l  536  f1imass  5753  tfrlem1  6287  phplem4dom  6840  phplem4on  6845  fisseneq  6909  suplub2ti  6978  omp1eomlem  7071  nnnninfeq  7104  nninfisol  7109  exmidontriim  7202  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  ltexnqq  7370  enq0tr  7396  addcmpblnq0  7405  mulcmpblnq0  7406  nnnq0lem1  7408  prssnql  7441  prmuloc  7528  prmuloc2  7529  mullocpr  7533  ltexprlemopu  7565  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  ltmprr  7604  archpr  7605  suplocexprlemloc  7683  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  ltsrprg  7709  srpospr  7745  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  negeu  8110  add20  8393  rimul  8504  apreap  8506  cru  8521  mulge0  8538  mulap0  8572  prodgt0  8768  ltmul12a  8776  ledivdiv  8806  lediv12a  8810  qapne  9598  qreccl  9601  xleaddadd  9844  ixxss12  9863  ioodisj  9950  fznlem  9997  elfz0fzfz0  10082  btwnzge0  10256  mulexpzap  10516  leexp1a  10531  expnbnd  10599  hashennnuni  10713  zfz1iso  10776  seq3coll  10777  resqrexlemga  10987  sqrtsq  11008  abs3lem  11075  cau3lem  11078  minmax  11193  xrmaxiflemval  11213  xrminmax  11228  climcau  11310  summodclem2  11345  fsumrelem  11434  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  fprodcl2lem  11568  fprodap0  11584  fprodrec  11592  fprodap0f  11599  fprodle  11603  dvdsle  11804  gcdsupex  11912  gcdsupcl  11913  bezoutlemmain  11953  bezoutlemzz  11957  dfgcd3  11965  dvdsmulgcd  11980  lcmcllem  12021  lcmgcdlem  12031  ncoprmgcdne1b  12043  qredeu  12051  oddpwdclemxy  12123  oddpwdclemdc  12127  pythagtriplem2  12220  pythagtrip  12237  pc2dvds  12283  pcz  12285  ctiunctlemfo  12394  unct  12397  mndpropd  12676  mhmeql  12707  neissex  12959  restbasg  12962  tgrest  12963  restopnb  12975  cnptopco  13016  metequiv2  13290  xmettx  13304  metcnpi3  13311  fsumcncntop  13350  elcncf2  13355  cncfmet  13373  dedekindeulemuub  13389  dedekindeulemlu  13393  dedekindicclemuub  13398  dedekindicclemlu  13402  limccnpcntop  13438  reeff1olem  13486  nninfalllem1  14041  apdiff  14080