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  5897  tfrlem1  6452  phplem4dom  7019  phplem4on  7025  fisseneq  7092  suplub2ti  7164  omp1eomlem  7257  nnnninfeq  7291  nninfisol  7296  exmidontriim  7403  addcmpblnq  7550  mulcmpblnq  7551  ordpipqqs  7557  ltexnqq  7591  enq0tr  7617  addcmpblnq0  7626  mulcmpblnq0  7627  nnnq0lem1  7629  prssnql  7662  prmuloc  7749  prmuloc2  7750  mullocpr  7754  ltexprlemopu  7786  ltexprlemrl  7793  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  ltmprr  7825  archpr  7826  suplocexprlemloc  7904  addcmpblnr  7922  mulcmpblnrlemg  7923  mulcmpblnr  7924  ltsrprg  7930  srpospr  7966  axcaucvglemres  8082  axpre-suploclemres  8084  axpre-suploc  8085  negeu  8333  add20  8617  rimul  8728  apreap  8730  cru  8745  mulge0  8762  mulap0  8797  prodgt0  8995  ltmul12a  9003  ledivdiv  9033  lediv12a  9037  qapne  9830  qreccl  9833  xleaddadd  10079  ixxss12  10098  ioodisj  10185  fznlem  10233  elfz0fzfz0  10318  btwnzge0  10515  seqf1og  10738  mulexpzap  10796  leexp1a  10811  expnbnd  10880  hashennnuni  10996  zfz1iso  11058  seq3coll  11059  swrdswrdlem  11231  pfxccatin12lem3  11259  resqrexlemga  11529  sqrtsq  11550  abs3lem  11617  cau3lem  11620  minmax  11736  xrmaxiflemval  11756  xrminmax  11771  climcau  11853  summodclem2  11888  fsumrelem  11977  cvgratz  12038  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  fprodcl2lem  12111  fprodap0  12127  fprodrec  12135  fprodap0f  12142  fprodle  12146  dvdsle  12350  bitsfzo  12461  bezoutlemmain  12514  bezoutlemzz  12518  dfgcd3  12526  dvdsmulgcd  12541  lcmcllem  12584  lcmgcdlem  12594  ncoprmgcdne1b  12606  qredeu  12614  oddpwdclemxy  12686  oddpwdclemdc  12690  pythagtriplem2  12784  pythagtrip  12801  pc2dvds  12848  pcz  12850  ctiunctlemfo  13005  unct  13008  sgrppropd  13441  mndpropd  13468  mhmeql  13520  mhmid  13647  mhmmnd  13648  mulgval  13654  issubg4m  13725  imasabl  13868  gsumfzconst  13873  reldvdsrsrg  14050  dvdsrmul1  14060  unitgrp  14074  neissex  14833  restbasg  14836  tgrest  14837  restopnb  14849  cnptopco  14890  metequiv2  15164  xmettx  15178  metcnpi3  15185  mpomulcn  15234  fsumcncntop  15235  elcncf2  15242  cncfmet  15260  dedekindeulemuub  15285  dedekindeulemlu  15289  dedekindicclemuub  15294  dedekindicclemlu  15298  limccnpcntop  15343  dvmptfsum  15393  reeff1olem  15439  lgsquad3  15757  nninfalllem1  16333  nninfnfiinf  16348  apdiff  16375