Theorem simplll 523

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simp-4l  531  f1imass  5742  tfrlem1  6276  phplem4dom  6828  phplem4on  6833  fisseneq  6897  suplub2ti  6966  omp1eomlem  7059  nnnninfeq  7092  nninfisol  7097  exmidontriim  7181  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  ltexnqq  7349  enq0tr  7375  addcmpblnq0  7384  mulcmpblnq0  7385  nnnq0lem1  7387  prssnql  7420  prmuloc  7507  prmuloc2  7508  mullocpr  7512  ltexprlemopu  7544  ltexprlemrl  7551  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  ltmprr  7583  archpr  7584  suplocexprlemloc  7662  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  ltsrprg  7688  srpospr  7724  axcaucvglemres  7840  axpre-suploclemres  7842  axpre-suploc  7843  negeu  8089  add20  8372  rimul  8483  apreap  8485  cru  8500  mulge0  8517  mulap0  8551  prodgt0  8747  ltmul12a  8755  ledivdiv  8785  lediv12a  8789  qapne  9577  qreccl  9580  xleaddadd  9823  ixxss12  9842  ioodisj  9929  fznlem  9976  elfz0fzfz0  10061  btwnzge0  10235  mulexpzap  10495  leexp1a  10510  expnbnd  10578  hashennnuni  10692  zfz1iso  10754  seq3coll  10755  resqrexlemga  10965  sqrtsq  10986  abs3lem  11053  cau3lem  11056  minmax  11171  xrmaxiflemval  11191  xrminmax  11206  climcau  11288  summodclem2  11323  fsumrelem  11412  cvgratz  11473  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  fprodcl2lem  11546  fprodap0  11562  fprodrec  11570  fprodap0f  11577  fprodle  11581  dvdsle  11782  gcdsupex  11890  gcdsupcl  11891  bezoutlemmain  11931  bezoutlemzz  11935  dfgcd3  11943  dvdsmulgcd  11958  lcmcllem  11999  lcmgcdlem  12009  ncoprmgcdne1b  12021  qredeu  12029  oddpwdclemxy  12101  oddpwdclemdc  12105  pythagtriplem2  12198  pythagtrip  12215  pc2dvds  12261  pcz  12263  ctiunctlemfo  12372  unct  12375  neissex  12805  restbasg  12808  tgrest  12809  restopnb  12821  cnptopco  12862  metequiv2  13136  xmettx  13150  metcnpi3  13157  fsumcncntop  13196  elcncf2  13201  cncfmet  13219  dedekindeulemuub  13235  dedekindeulemlu  13239  dedekindicclemuub  13244  dedekindicclemlu  13248  limccnpcntop  13284  reeff1olem  13332  nninfalllem1  13888  apdiff  13927