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  5842  tfrlem1  6393  phplem4dom  6958  phplem4on  6963  fisseneq  7030  suplub2ti  7102  omp1eomlem  7195  nnnninfeq  7229  nninfisol  7234  exmidontriim  7336  addcmpblnq  7479  mulcmpblnq  7480  ordpipqqs  7486  ltexnqq  7520  enq0tr  7546  addcmpblnq0  7555  mulcmpblnq0  7556  nnnq0lem1  7558  prssnql  7591  prmuloc  7678  prmuloc2  7679  mullocpr  7683  ltexprlemopu  7715  ltexprlemrl  7722  ltexprlemru  7724  addcanprleml  7726  addcanprlemu  7727  ltmprr  7754  archpr  7755  suplocexprlemloc  7833  addcmpblnr  7851  mulcmpblnrlemg  7852  mulcmpblnr  7853  ltsrprg  7859  srpospr  7895  axcaucvglemres  8011  axpre-suploclemres  8013  axpre-suploc  8014  negeu  8262  add20  8546  rimul  8657  apreap  8659  cru  8674  mulge0  8691  mulap0  8726  prodgt0  8924  ltmul12a  8932  ledivdiv  8962  lediv12a  8966  qapne  9759  qreccl  9762  xleaddadd  10008  ixxss12  10027  ioodisj  10114  fznlem  10162  elfz0fzfz0  10247  btwnzge0  10441  seqf1og  10664  mulexpzap  10722  leexp1a  10737  expnbnd  10806  hashennnuni  10922  zfz1iso  10984  seq3coll  10985  resqrexlemga  11305  sqrtsq  11326  abs3lem  11393  cau3lem  11396  minmax  11512  xrmaxiflemval  11532  xrminmax  11547  climcau  11629  summodclem2  11664  fsumrelem  11753  cvgratz  11814  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  fprodcl2lem  11887  fprodap0  11903  fprodrec  11911  fprodap0f  11918  fprodle  11922  dvdsle  12126  bitsfzo  12237  bezoutlemmain  12290  bezoutlemzz  12294  dfgcd3  12302  dvdsmulgcd  12317  lcmcllem  12360  lcmgcdlem  12370  ncoprmgcdne1b  12382  qredeu  12390  oddpwdclemxy  12462  oddpwdclemdc  12466  pythagtriplem2  12560  pythagtrip  12577  pc2dvds  12624  pcz  12626  ctiunctlemfo  12781  unct  12784  sgrppropd  13216  mndpropd  13243  mhmeql  13295  mhmid  13422  mhmmnd  13423  mulgval  13429  issubg4m  13500  imasabl  13643  gsumfzconst  13648  reldvdsrsrg  13825  dvdsrmul1  13835  unitgrp  13849  neissex  14608  restbasg  14611  tgrest  14612  restopnb  14624  cnptopco  14665  metequiv2  14939  xmettx  14953  metcnpi3  14960  mpomulcn  15009  fsumcncntop  15010  elcncf2  15017  cncfmet  15035  dedekindeulemuub  15060  dedekindeulemlu  15064  dedekindicclemuub  15069  dedekindicclemlu  15073  limccnpcntop  15118  dvmptfsum  15168  reeff1olem  15214  lgsquad3  15532  nninfalllem1  15907  nninfnfiinf  15922  apdiff  15949