Theorem simplll 523

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 480	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  531  f1imass  5736  tfrlem1  6267  phplem4dom  6819  phplem4on  6824  fisseneq  6888  suplub2ti  6957  omp1eomlem  7050  nnnninfeq  7083  nninfisol  7088  exmidontriim  7172  addcmpblnq  7299  mulcmpblnq  7300  ordpipqqs  7306  ltexnqq  7340  enq0tr  7366  addcmpblnq0  7375  mulcmpblnq0  7376  nnnq0lem1  7378  prssnql  7411  prmuloc  7498  prmuloc2  7499  mullocpr  7503  ltexprlemopu  7535  ltexprlemrl  7542  ltexprlemru  7544  addcanprleml  7546  addcanprlemu  7547  ltmprr  7574  archpr  7575  suplocexprlemloc  7653  addcmpblnr  7671  mulcmpblnrlemg  7672  mulcmpblnr  7673  ltsrprg  7679  srpospr  7715  axcaucvglemres  7831  axpre-suploclemres  7833  axpre-suploc  7834  negeu  8080  add20  8363  rimul  8474  apreap  8476  cru  8491  mulge0  8508  mulap0  8542  prodgt0  8738  ltmul12a  8746  ledivdiv  8776  lediv12a  8780  qapne  9568  qreccl  9571  xleaddadd  9814  ixxss12  9833  ioodisj  9920  fznlem  9966  elfz0fzfz0  10051  btwnzge0  10225  mulexpzap  10485  leexp1a  10500  expnbnd  10567  hashennnuni  10681  zfz1iso  10740  seq3coll  10741  resqrexlemga  10951  sqrtsq  10972  abs3lem  11039  cau3lem  11042  minmax  11157  xrmaxiflemval  11177  xrminmax  11192  climcau  11274  summodclem2  11309  fsumrelem  11398  cvgratz  11459  mertenslemi1  11462  mertenslem2  11463  mertensabs  11464  fprodcl2lem  11532  fprodap0  11548  fprodrec  11556  fprodap0f  11563  fprodle  11567  dvdsle  11767  gcdsupex  11875  gcdsupcl  11876  bezoutlemmain  11916  bezoutlemzz  11920  dfgcd3  11928  dvdsmulgcd  11943  lcmcllem  11978  lcmgcdlem  11988  ncoprmgcdne1b  12000  qredeu  12008  oddpwdclemxy  12078  oddpwdclemdc  12082  pythagtriplem2  12175  pythagtrip  12192  pc2dvds  12238  pcz  12240  ctiunctlemfo  12309  unct  12312  neissex  12706  restbasg  12709  tgrest  12710  restopnb  12722  cnptopco  12763  metequiv2  13037  xmettx  13051  metcnpi3  13058  fsumcncntop  13097  elcncf2  13102  cncfmet  13120  dedekindeulemuub  13136  dedekindeulemlu  13140  dedekindicclemuub  13145  dedekindicclemlu  13149  limccnpcntop  13185  reeff1olem  13233  nninfalllem1  13722  apdiff  13761