Theorem simplll 539

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 492	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-4l  547  f1imass  5980  suppcofn  6506  tfrlem1  6579  phplem4dom  7163  phplem4on  7169  fisseneq  7242  suplub2ti  7341  omp1eomlem  7434  nnnninfeq  7468  nninfisol  7473  exmidontriim  7581  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  ltexnqq  7775  enq0tr  7801  addcmpblnq0  7810  mulcmpblnq0  7811  nnnq0lem1  7813  prssnql  7846  prmuloc  7933  prmuloc2  7934  mullocpr  7938  ltexprlemopu  7970  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  archpr  8010  suplocexprlemloc  8088  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  ltsrprg  8114  srpospr  8150  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  negeu  8518  add20  8803  rimul  8915  apreap  8917  cru  8932  mulge0  8949  mulap0  8984  prodgt0  9184  ltmul12a  9192  ledivdiv  9222  lediv12a  9226  qapne  10048  qreccl  10051  irraddap  10056  xleaddadd  10299  ixxss12  10318  ioodisj  10405  fznlem  10455  elfz0fzfz0  10543  btwnzge0  10748  seqf1og  10971  mulexpzap  11029  leexp1a  11044  expnbnd  11114  hashennnuni  11232  hashf1lem2  11300  zfz1iso  11307  seq3coll  11308  swrdswrdlem  11490  pfxccatin12lem3  11518  resqrexlemga  11803  sqrtsq  11824  abs3lem  11892  cau3lem  11895  minmax  12011  xrmaxiflemval  12032  xrminmax  12047  climcau  12129  summodclem2  12165  fsumrelem  12254  cvgratz  12315  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  fprodcl2lem  12388  fprodap0  12404  fprodrec  12412  fprodap0f  12419  fprodle  12423  dvdsle  12627  bitsfzo  12738  bezoutlemmain  12791  bezoutlemzz  12795  dfgcd3  12803  dvdsmulgcd  12818  lcmcllem  12861  lcmgcdlem  12871  ncoprmgcdne1b  12883  qredeu  12891  pwbdvdseu  12963  nnmaxpwlemparts  12968  pythagtriplem2  13065  pythagtrip  13082  pc2dvds  13129  pcz  13131  ctiunctlemfo  13379  unct  13382  sgrppropd  13777  mndpropd  13802  mhmeql  13848  mhmid  13967  mhmmnd  13968  mulgval  13974  issubg4m  14045  imasabl  14189  gzsumconst  14192  gsumzfi  14207  gsummptfidmadd  14210  dvdsrmul1  14458  unitgrp  14472  aprlring  14649  gsumfsum  14972  issubassa2  15084  neissex  15315  restbasg  15318  tgrest  15319  restopnb  15331  cnptopco  15372  metequiv2  15646  xmettx  15660  metcnpi3  15667  mpomulcn  15716  fsumcncntop  15717  elcncf2  15724  cncfmet  15742  dedekindeulemuub  15767  dedekindeulemlu  15771  dedekindicclemuub  15776  dedekindicclemlu  15780  limccnpcntop  15825  dvmptfsum  15875  reeff1olem  15921  lgsquad3  16301  clwwlkccatlem  16739  nninfalllem1  17149  nninfnfiinf  17164  apdiff  17195