Theorem simplll 535

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  543  f1imass  5915  tfrlem1  6474  phplem4dom  7048  phplem4on  7054  fisseneq  7127  suplub2ti  7200  omp1eomlem  7293  nnnninfeq  7327  nninfisol  7332  exmidontriim  7440  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  ltexnqq  7628  enq0tr  7654  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  prssnql  7699  prmuloc  7786  prmuloc2  7787  mullocpr  7791  ltexprlemopu  7823  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  archpr  7863  suplocexprlemloc  7941  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  srpospr  8003  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  negeu  8370  add20  8654  rimul  8765  apreap  8767  cru  8782  mulge0  8799  mulap0  8834  prodgt0  9032  ltmul12a  9040  ledivdiv  9070  lediv12a  9074  qapne  9873  qreccl  9876  xleaddadd  10122  ixxss12  10141  ioodisj  10228  fznlem  10276  elfz0fzfz0  10361  btwnzge0  10561  seqf1og  10784  mulexpzap  10842  leexp1a  10857  expnbnd  10926  hashennnuni  11042  zfz1iso  11106  seq3coll  11107  swrdswrdlem  11289  pfxccatin12lem3  11317  resqrexlemga  11601  sqrtsq  11622  abs3lem  11689  cau3lem  11692  minmax  11808  xrmaxiflemval  11828  xrminmax  11843  climcau  11925  summodclem2  11961  fsumrelem  12050  cvgratz  12111  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  fprodcl2lem  12184  fprodap0  12200  fprodrec  12208  fprodap0f  12215  fprodle  12219  dvdsle  12423  bitsfzo  12534  bezoutlemmain  12587  bezoutlemzz  12591  dfgcd3  12599  dvdsmulgcd  12614  lcmcllem  12657  lcmgcdlem  12667  ncoprmgcdne1b  12679  qredeu  12687  oddpwdclemxy  12759  oddpwdclemdc  12763  pythagtriplem2  12857  pythagtrip  12874  pc2dvds  12921  pcz  12923  ctiunctlemfo  13078  unct  13081  sgrppropd  13514  mndpropd  13541  mhmeql  13593  mhmid  13720  mhmmnd  13721  mulgval  13727  issubg4m  13798  imasabl  13941  gsumfzconst  13946  dvdsrmul1  14135  unitgrp  14149  neissex  14908  restbasg  14911  tgrest  14912  restopnb  14924  cnptopco  14965  metequiv2  15239  xmettx  15253  metcnpi3  15260  mpomulcn  15309  fsumcncntop  15310  elcncf2  15317  cncfmet  15335  dedekindeulemuub  15360  dedekindeulemlu  15364  dedekindicclemuub  15369  dedekindicclemlu  15373  limccnpcntop  15418  dvmptfsum  15468  reeff1olem  15514  lgsquad3  15832  clwwlkccatlem  16270  nninfalllem1  16661  nninfnfiinf  16676  apdiff  16703