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  8517  add20  8802  rimul  8913  apreap  8915  cru  8930  mulge0  8947  mulap0  8982  prodgt0  9182  ltmul12a  9190  ledivdiv  9220  lediv12a  9224  qapne  10039  qreccl  10042  xleaddadd  10289  ixxss12  10308  ioodisj  10395  fznlem  10445  elfz0fzfz0  10533  btwnzge0  10735  seqf1og  10958  mulexpzap  11016  leexp1a  11031  expnbnd  11101  hashennnuni  11218  hashf1lem2  11286  zfz1iso  11293  seq3coll  11294  swrdswrdlem  11476  pfxccatin12lem3  11504  resqrexlemga  11789  sqrtsq  11810  abs3lem  11877  cau3lem  11880  minmax  11996  xrmaxiflemval  12016  xrminmax  12031  climcau  12113  summodclem2  12149  fsumrelem  12238  cvgratz  12299  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  fprodcl2lem  12372  fprodap0  12388  fprodrec  12396  fprodap0f  12403  fprodle  12407  dvdsle  12611  bitsfzo  12722  bezoutlemmain  12775  bezoutlemzz  12779  dfgcd3  12787  dvdsmulgcd  12802  lcmcllem  12845  lcmgcdlem  12855  ncoprmgcdne1b  12867  qredeu  12875  oddpwdclemxy  12947  oddpwdclemdc  12951  pythagtriplem2  13045  pythagtrip  13062  pc2dvds  13109  pcz  13111  ctiunctlemfo  13330  unct  13333  sgrppropd  13728  mndpropd  13753  mhmeql  13799  mhmid  13918  mhmmnd  13919  mulgval  13925  issubg4m  13996  imasabl  14140  gzsumconst  14143  gsumzfi  14158  gsummptfidmadd  14161  dvdsrmul1  14409  unitgrp  14423  aprlring  14600  gsumfsum  14923  issubassa2  15035  neissex  15266  restbasg  15269  tgrest  15270  restopnb  15282  cnptopco  15323  metequiv2  15597  xmettx  15611  metcnpi3  15618  mpomulcn  15667  fsumcncntop  15668  elcncf2  15675  cncfmet  15693  dedekindeulemuub  15718  dedekindeulemlu  15722  dedekindicclemuub  15727  dedekindicclemlu  15731  limccnpcntop  15776  dvmptfsum  15826  reeff1olem  15872  lgsquad3  16203  clwwlkccatlem  16641  nninfalllem1  17051  nninfnfiinf  17066  apdiff  17097