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  5953  suppcofn  6479  tfrlem1  6552  phplem4dom  7129  phplem4on  7135  fisseneq  7208  suplub2ti  7305  omp1eomlem  7398  nnnninfeq  7432  nninfisol  7437  exmidontriim  7545  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  ltexnqq  7739  enq0tr  7765  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  prssnql  7810  prmuloc  7897  prmuloc2  7898  mullocpr  7902  ltexprlemopu  7934  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  archpr  7974  suplocexprlemloc  8052  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  srpospr  8114  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  negeu  8480  add20  8765  rimul  8876  apreap  8878  cru  8893  mulge0  8910  mulap0  8945  prodgt0  9143  ltmul12a  9151  ledivdiv  9181  lediv12a  9185  qapne  9989  qreccl  9992  xleaddadd  10239  ixxss12  10258  ioodisj  10345  fznlem  10395  elfz0fzfz0  10482  btwnzge0  10684  seqf1og  10907  mulexpzap  10965  leexp1a  10980  expnbnd  11050  hashennnuni  11167  zfz1iso  11238  seq3coll  11239  swrdswrdlem  11421  pfxccatin12lem3  11449  resqrexlemga  11733  sqrtsq  11754  abs3lem  11821  cau3lem  11824  minmax  11940  xrmaxiflemval  11960  xrminmax  11975  climcau  12057  summodclem2  12093  fsumrelem  12182  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  fprodcl2lem  12316  fprodap0  12332  fprodrec  12340  fprodap0f  12347  fprodle  12351  dvdsle  12555  bitsfzo  12666  bezoutlemmain  12719  bezoutlemzz  12723  dfgcd3  12731  dvdsmulgcd  12746  lcmcllem  12789  lcmgcdlem  12799  ncoprmgcdne1b  12811  qredeu  12819  oddpwdclemxy  12891  oddpwdclemdc  12895  pythagtriplem2  12989  pythagtrip  13006  pc2dvds  13053  pcz  13055  ctiunctlemfo  13274  unct  13277  sgrppropd  13676  mndpropd  13701  mhmeql  13747  mhmid  13868  mhmmnd  13869  mulgval  13875  issubg4m  13946  imasabl  14089  gsumfzconst  14094  gfsumz  14109  dvdsrmul1  14347  unitgrp  14361  aprlring  14538  neissex  15156  restbasg  15159  tgrest  15160  restopnb  15172  cnptopco  15213  metequiv2  15487  xmettx  15501  metcnpi3  15508  mpomulcn  15557  fsumcncntop  15558  elcncf2  15565  cncfmet  15583  dedekindeulemuub  15608  dedekindeulemlu  15612  dedekindicclemuub  15617  dedekindicclemlu  15621  limccnpcntop  15666  dvmptfsum  15716  reeff1olem  15762  lgsquad3  16083  clwwlkccatlem  16521  nninfalllem1  16912  nninfnfiinf  16927  apdiff  16958