Theorem simplll 535

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  543  f1imass  5947  suppcofn  6466  tfrlem1  6539  phplem4dom  7116  phplem4on  7122  fisseneq  7195  suplub2ti  7292  omp1eomlem  7385  nnnninfeq  7419  nninfisol  7424  exmidontriim  7532  addcmpblnq  7682  mulcmpblnq  7683  ordpipqqs  7689  ltexnqq  7723  enq0tr  7749  addcmpblnq0  7758  mulcmpblnq0  7759  nnnq0lem1  7761  prssnql  7794  prmuloc  7881  prmuloc2  7882  mullocpr  7886  ltexprlemopu  7918  ltexprlemrl  7925  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  ltmprr  7957  archpr  7958  suplocexprlemloc  8036  addcmpblnr  8054  mulcmpblnrlemg  8055  mulcmpblnr  8056  ltsrprg  8062  srpospr  8098  axcaucvglemres  8214  axpre-suploclemres  8216  axpre-suploc  8217  negeu  8464  add20  8748  rimul  8859  apreap  8861  cru  8876  mulge0  8893  mulap0  8928  prodgt0  9126  ltmul12a  9134  ledivdiv  9164  lediv12a  9168  qapne  9971  qreccl  9974  xleaddadd  10220  ixxss12  10239  ioodisj  10326  fznlem  10375  elfz0fzfz0  10460  btwnzge0  10660  seqf1og  10883  mulexpzap  10941  leexp1a  10956  expnbnd  11025  hashennnuni  11142  zfz1iso  11213  seq3coll  11214  swrdswrdlem  11396  pfxccatin12lem3  11424  resqrexlemga  11708  sqrtsq  11729  abs3lem  11796  cau3lem  11799  minmax  11915  xrmaxiflemval  11935  xrminmax  11950  climcau  12032  summodclem2  12068  fsumrelem  12157  cvgratz  12218  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  fprodcl2lem  12291  fprodap0  12307  fprodrec  12315  fprodap0f  12322  fprodle  12326  dvdsle  12530  bitsfzo  12641  bezoutlemmain  12694  bezoutlemzz  12698  dfgcd3  12706  dvdsmulgcd  12721  lcmcllem  12764  lcmgcdlem  12774  ncoprmgcdne1b  12786  qredeu  12794  oddpwdclemxy  12866  oddpwdclemdc  12870  pythagtriplem2  12964  pythagtrip  12981  pc2dvds  13028  pcz  13030  ctiunctlemfo  13190  unct  13193  sgrppropd  13626  mndpropd  13653  mhmeql  13705  mhmid  13832  mhmmnd  13833  mulgval  13839  issubg4m  13910  imasabl  14053  gsumfzconst  14058  dvdsrmul1  14247  unitgrp  14261  aprlring  14434  neissex  15030  restbasg  15033  tgrest  15034  restopnb  15046  cnptopco  15087  metequiv2  15361  xmettx  15375  metcnpi3  15382  mpomulcn  15431  fsumcncntop  15432  elcncf2  15439  cncfmet  15457  dedekindeulemuub  15482  dedekindeulemlu  15486  dedekindicclemuub  15491  dedekindicclemlu  15495  limccnpcntop  15540  dvmptfsum  15590  reeff1olem  15636  lgsquad3  15957  clwwlkccatlem  16395  nninfalllem1  16786  nninfnfiinf  16801  apdiff  16832  gfsumz  16869