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  5904  tfrlem1  6460  phplem4dom  7031  phplem4on  7037  fisseneq  7107  suplub2ti  7179  omp1eomlem  7272  nnnninfeq  7306  nninfisol  7311  exmidontriim  7418  addcmpblnq  7565  mulcmpblnq  7566  ordpipqqs  7572  ltexnqq  7606  enq0tr  7632  addcmpblnq0  7641  mulcmpblnq0  7642  nnnq0lem1  7644  prssnql  7677  prmuloc  7764  prmuloc2  7765  mullocpr  7769  ltexprlemopu  7801  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  ltmprr  7840  archpr  7841  suplocexprlemloc  7919  addcmpblnr  7937  mulcmpblnrlemg  7938  mulcmpblnr  7939  ltsrprg  7945  srpospr  7981  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  negeu  8348  add20  8632  rimul  8743  apreap  8745  cru  8760  mulge0  8777  mulap0  8812  prodgt0  9010  ltmul12a  9018  ledivdiv  9048  lediv12a  9052  qapne  9846  qreccl  9849  xleaddadd  10095  ixxss12  10114  ioodisj  10201  fznlem  10249  elfz0fzfz0  10334  btwnzge0  10532  seqf1og  10755  mulexpzap  10813  leexp1a  10828  expnbnd  10897  hashennnuni  11013  zfz1iso  11076  seq3coll  11077  swrdswrdlem  11251  pfxccatin12lem3  11279  resqrexlemga  11549  sqrtsq  11570  abs3lem  11637  cau3lem  11640  minmax  11756  xrmaxiflemval  11776  xrminmax  11791  climcau  11873  summodclem2  11908  fsumrelem  11997  cvgratz  12058  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  fprodcl2lem  12131  fprodap0  12147  fprodrec  12155  fprodap0f  12162  fprodle  12166  dvdsle  12370  bitsfzo  12481  bezoutlemmain  12534  bezoutlemzz  12538  dfgcd3  12546  dvdsmulgcd  12561  lcmcllem  12604  lcmgcdlem  12614  ncoprmgcdne1b  12626  qredeu  12634  oddpwdclemxy  12706  oddpwdclemdc  12710  pythagtriplem2  12804  pythagtrip  12821  pc2dvds  12868  pcz  12870  ctiunctlemfo  13025  unct  13028  sgrppropd  13461  mndpropd  13488  mhmeql  13540  mhmid  13667  mhmmnd  13668  mulgval  13674  issubg4m  13745  imasabl  13888  gsumfzconst  13893  dvdsrmul1  14081  unitgrp  14095  neissex  14854  restbasg  14857  tgrest  14858  restopnb  14870  cnptopco  14911  metequiv2  15185  xmettx  15199  metcnpi3  15206  mpomulcn  15255  fsumcncntop  15256  elcncf2  15263  cncfmet  15281  dedekindeulemuub  15306  dedekindeulemlu  15310  dedekindicclemuub  15315  dedekindicclemlu  15319  limccnpcntop  15364  dvmptfsum  15414  reeff1olem  15460  lgsquad3  15778  clwwlkccatlem  16137  nninfalllem1  16434  nninfnfiinf  16449  apdiff  16476