Theorem simplll 533

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  simp-4l  541  f1imass  5817  tfrlem1  6361  phplem4dom  6918  phplem4on  6923  fisseneq  6988  suplub2ti  7060  omp1eomlem  7153  nnnninfeq  7187  nninfisol  7192  exmidontriim  7285  addcmpblnq  7427  mulcmpblnq  7428  ordpipqqs  7434  ltexnqq  7468  enq0tr  7494  addcmpblnq0  7503  mulcmpblnq0  7504  nnnq0lem1  7506  prssnql  7539  prmuloc  7626  prmuloc2  7627  mullocpr  7631  ltexprlemopu  7663  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  ltmprr  7702  archpr  7703  suplocexprlemloc  7781  addcmpblnr  7799  mulcmpblnrlemg  7800  mulcmpblnr  7801  ltsrprg  7807  srpospr  7843  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  negeu  8210  add20  8493  rimul  8604  apreap  8606  cru  8621  mulge0  8638  mulap0  8673  prodgt0  8871  ltmul12a  8879  ledivdiv  8909  lediv12a  8913  qapne  9704  qreccl  9707  xleaddadd  9953  ixxss12  9972  ioodisj  10059  fznlem  10107  elfz0fzfz0  10192  btwnzge0  10369  seqf1og  10592  mulexpzap  10650  leexp1a  10665  expnbnd  10734  hashennnuni  10850  zfz1iso  10912  seq3coll  10913  resqrexlemga  11167  sqrtsq  11188  abs3lem  11255  cau3lem  11258  minmax  11373  xrmaxiflemval  11393  xrminmax  11408  climcau  11490  summodclem2  11525  fsumrelem  11614  cvgratz  11675  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  fprodcl2lem  11748  fprodap0  11764  fprodrec  11772  fprodap0f  11779  fprodle  11783  dvdsle  11986  bezoutlemmain  12135  bezoutlemzz  12139  dfgcd3  12147  dvdsmulgcd  12162  lcmcllem  12205  lcmgcdlem  12215  ncoprmgcdne1b  12227  qredeu  12235  oddpwdclemxy  12307  oddpwdclemdc  12311  pythagtriplem2  12404  pythagtrip  12421  pc2dvds  12468  pcz  12470  ctiunctlemfo  12596  unct  12599  sgrppropd  12996  mndpropd  13021  mhmeql  13064  mhmid  13185  mhmmnd  13186  mulgval  13192  issubg4m  13263  imasabl  13406  gsumfzconst  13411  reldvdsrsrg  13588  dvdsrmul1  13598  unitgrp  13612  neissex  14333  restbasg  14336  tgrest  14337  restopnb  14349  cnptopco  14390  metequiv2  14664  xmettx  14678  metcnpi3  14685  fsumcncntop  14724  elcncf2  14729  cncfmet  14747  dedekindeulemuub  14771  dedekindeulemlu  14775  dedekindicclemuub  14780  dedekindicclemlu  14784  limccnpcntop  14829  reeff1olem  14906  nninfalllem1  15498  apdiff  15538