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  5910  tfrlem1  6469  phplem4dom  7043  phplem4on  7049  fisseneq  7119  suplub2ti  7191  omp1eomlem  7284  nnnninfeq  7318  nninfisol  7323  exmidontriim  7430  addcmpblnq  7577  mulcmpblnq  7578  ordpipqqs  7584  ltexnqq  7618  enq0tr  7644  addcmpblnq0  7653  mulcmpblnq0  7654  nnnq0lem1  7656  prssnql  7689  prmuloc  7776  prmuloc2  7777  mullocpr  7781  ltexprlemopu  7813  ltexprlemrl  7820  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  ltmprr  7852  archpr  7853  suplocexprlemloc  7931  addcmpblnr  7949  mulcmpblnrlemg  7950  mulcmpblnr  7951  ltsrprg  7957  srpospr  7993  axcaucvglemres  8109  axpre-suploclemres  8111  axpre-suploc  8112  negeu  8360  add20  8644  rimul  8755  apreap  8757  cru  8772  mulge0  8789  mulap0  8824  prodgt0  9022  ltmul12a  9030  ledivdiv  9060  lediv12a  9064  qapne  9863  qreccl  9866  xleaddadd  10112  ixxss12  10131  ioodisj  10218  fznlem  10266  elfz0fzfz0  10351  btwnzge0  10550  seqf1og  10773  mulexpzap  10831  leexp1a  10846  expnbnd  10915  hashennnuni  11031  zfz1iso  11095  seq3coll  11096  swrdswrdlem  11275  pfxccatin12lem3  11303  resqrexlemga  11574  sqrtsq  11595  abs3lem  11662  cau3lem  11665  minmax  11781  xrmaxiflemval  11801  xrminmax  11816  climcau  11898  summodclem2  11933  fsumrelem  12022  cvgratz  12083  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  fprodcl2lem  12156  fprodap0  12172  fprodrec  12180  fprodap0f  12187  fprodle  12191  dvdsle  12395  bitsfzo  12506  bezoutlemmain  12559  bezoutlemzz  12563  dfgcd3  12571  dvdsmulgcd  12586  lcmcllem  12629  lcmgcdlem  12639  ncoprmgcdne1b  12651  qredeu  12659  oddpwdclemxy  12731  oddpwdclemdc  12735  pythagtriplem2  12829  pythagtrip  12846  pc2dvds  12893  pcz  12895  ctiunctlemfo  13050  unct  13053  sgrppropd  13486  mndpropd  13513  mhmeql  13565  mhmid  13692  mhmmnd  13693  mulgval  13699  issubg4m  13770  imasabl  13913  gsumfzconst  13918  dvdsrmul1  14106  unitgrp  14120  neissex  14879  restbasg  14882  tgrest  14883  restopnb  14895  cnptopco  14936  metequiv2  15210  xmettx  15224  metcnpi3  15231  mpomulcn  15280  fsumcncntop  15281  elcncf2  15288  cncfmet  15306  dedekindeulemuub  15331  dedekindeulemlu  15335  dedekindicclemuub  15340  dedekindicclemlu  15344  limccnpcntop  15389  dvmptfsum  15439  reeff1olem  15485  lgsquad3  15803  clwwlkccatlem  16195  nninfalllem1  16546  nninfnfiinf  16561  apdiff  16588