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 )

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  547  f1imass  5970  suppcofn  6496  tfrlem1  6569  phplem4dom  7153  phplem4on  7159  fisseneq  7232  suplub2ti  7331  omp1eomlem  7424  nnnninfeq  7458  nninfisol  7463  exmidontriim  7571  addcmpblnq  7724  mulcmpblnq  7725  ordpipqqs  7731  ltexnqq  7765  enq0tr  7791  addcmpblnq0  7800  mulcmpblnq0  7801  nnnq0lem1  7803  prssnql  7836  prmuloc  7923  prmuloc2  7924  mullocpr  7928  ltexprlemopu  7960  ltexprlemrl  7967  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  ltmprr  7999  archpr  8000  suplocexprlemloc  8078  addcmpblnr  8096  mulcmpblnrlemg  8097  mulcmpblnr  8098  ltsrprg  8104  srpospr  8140  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  negeu  8507  add20  8792  rimul  8903  apreap  8905  cru  8920  mulge0  8937  mulap0  8972  prodgt0  9172  ltmul12a  9180  ledivdiv  9210  lediv12a  9214  qapne  10018  qreccl  10021  xleaddadd  10268  ixxss12  10287  ioodisj  10374  fznlem  10424  elfz0fzfz0  10511  btwnzge0  10713  seqf1og  10936  mulexpzap  10994  leexp1a  11009  expnbnd  11079  hashennnuni  11196  hashf1lem2  11264  zfz1iso  11271  seq3coll  11272  swrdswrdlem  11454  pfxccatin12lem3  11482  resqrexlemga  11767  sqrtsq  11788  abs3lem  11855  cau3lem  11858  minmax  11974  xrmaxiflemval  11994  xrminmax  12009  climcau  12091  summodclem2  12127  fsumrelem  12216  cvgratz  12277  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  fprodcl2lem  12350  fprodap0  12366  fprodrec  12374  fprodap0f  12381  fprodle  12385  dvdsle  12589  bitsfzo  12700  bezoutlemmain  12753  bezoutlemzz  12757  dfgcd3  12765  dvdsmulgcd  12780  lcmcllem  12823  lcmgcdlem  12833  ncoprmgcdne1b  12845  qredeu  12853  oddpwdclemxy  12925  oddpwdclemdc  12929  pythagtriplem2  13023  pythagtrip  13040  pc2dvds  13087  pcz  13089  ctiunctlemfo  13308  unct  13311  sgrppropd  13705  mndpropd  13730  mhmeql  13776  mhmid  13895  mhmmnd  13896  mulgval  13902  issubg4m  13973  imasabl  14117  gzsumconst  14120  gsumzfi  14135  gsummptfidmadd  14138  dvdsrmul1  14382  unitgrp  14396  aprlring  14573  gsumfsum  14895  neissex  15189  restbasg  15192  tgrest  15193  restopnb  15205  cnptopco  15246  metequiv2  15520  xmettx  15534  metcnpi3  15541  mpomulcn  15590  fsumcncntop  15591  elcncf2  15598  cncfmet  15616  dedekindeulemuub  15641  dedekindeulemlu  15645  dedekindicclemuub  15650  dedekindicclemlu  15654  limccnpcntop  15699  dvmptfsum  15749  reeff1olem  15795  lgsquad3  16117  clwwlkccatlem  16555  nninfalllem1  16956  nninfnfiinf  16971  apdiff  17002