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  5856  tfrlem1  6407  phplem4dom  6974  phplem4on  6979  fisseneq  7046  suplub2ti  7118  omp1eomlem  7211  nnnninfeq  7245  nninfisol  7250  exmidontriim  7353  addcmpblnq  7500  mulcmpblnq  7501  ordpipqqs  7507  ltexnqq  7541  enq0tr  7567  addcmpblnq0  7576  mulcmpblnq0  7577  nnnq0lem1  7579  prssnql  7612  prmuloc  7699  prmuloc2  7700  mullocpr  7704  ltexprlemopu  7736  ltexprlemrl  7743  ltexprlemru  7745  addcanprleml  7747  addcanprlemu  7748  ltmprr  7775  archpr  7776  suplocexprlemloc  7854  addcmpblnr  7872  mulcmpblnrlemg  7873  mulcmpblnr  7874  ltsrprg  7880  srpospr  7916  axcaucvglemres  8032  axpre-suploclemres  8034  axpre-suploc  8035  negeu  8283  add20  8567  rimul  8678  apreap  8680  cru  8695  mulge0  8712  mulap0  8747  prodgt0  8945  ltmul12a  8953  ledivdiv  8983  lediv12a  8987  qapne  9780  qreccl  9783  xleaddadd  10029  ixxss12  10048  ioodisj  10135  fznlem  10183  elfz0fzfz0  10268  btwnzge0  10465  seqf1og  10688  mulexpzap  10746  leexp1a  10761  expnbnd  10830  hashennnuni  10946  zfz1iso  11008  seq3coll  11009  swrdswrdlem  11180  resqrexlemga  11409  sqrtsq  11430  abs3lem  11497  cau3lem  11500  minmax  11616  xrmaxiflemval  11636  xrminmax  11651  climcau  11733  summodclem2  11768  fsumrelem  11857  cvgratz  11918  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  fprodcl2lem  11991  fprodap0  12007  fprodrec  12015  fprodap0f  12022  fprodle  12026  dvdsle  12230  bitsfzo  12341  bezoutlemmain  12394  bezoutlemzz  12398  dfgcd3  12406  dvdsmulgcd  12421  lcmcllem  12464  lcmgcdlem  12474  ncoprmgcdne1b  12486  qredeu  12494  oddpwdclemxy  12566  oddpwdclemdc  12570  pythagtriplem2  12664  pythagtrip  12681  pc2dvds  12728  pcz  12730  ctiunctlemfo  12885  unct  12888  sgrppropd  13320  mndpropd  13347  mhmeql  13399  mhmid  13526  mhmmnd  13527  mulgval  13533  issubg4m  13604  imasabl  13747  gsumfzconst  13752  reldvdsrsrg  13929  dvdsrmul1  13939  unitgrp  13953  neissex  14712  restbasg  14715  tgrest  14716  restopnb  14728  cnptopco  14769  metequiv2  15043  xmettx  15057  metcnpi3  15064  mpomulcn  15113  fsumcncntop  15114  elcncf2  15121  cncfmet  15139  dedekindeulemuub  15164  dedekindeulemlu  15168  dedekindicclemuub  15173  dedekindicclemlu  15177  limccnpcntop  15222  dvmptfsum  15272  reeff1olem  15318  lgsquad3  15636  nninfalllem1  16086  nninfnfiinf  16101  apdiff  16128