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  5768  tfrlem1  6302  phplem4dom  6855  phplem4on  6860  fisseneq  6924  suplub2ti  6993  omp1eomlem  7086  nnnninfeq  7119  nninfisol  7124  exmidontriim  7217  addcmpblnq  7344  mulcmpblnq  7345  ordpipqqs  7351  ltexnqq  7385  enq0tr  7411  addcmpblnq0  7420  mulcmpblnq0  7421  nnnq0lem1  7423  prssnql  7456  prmuloc  7543  prmuloc2  7544  mullocpr  7548  ltexprlemopu  7580  ltexprlemrl  7587  ltexprlemru  7589  addcanprleml  7591  addcanprlemu  7592  ltmprr  7619  archpr  7620  suplocexprlemloc  7698  addcmpblnr  7716  mulcmpblnrlemg  7717  mulcmpblnr  7718  ltsrprg  7724  srpospr  7760  axcaucvglemres  7876  axpre-suploclemres  7878  axpre-suploc  7879  negeu  8125  add20  8408  rimul  8519  apreap  8521  cru  8536  mulge0  8553  mulap0  8587  prodgt0  8785  ltmul12a  8793  ledivdiv  8823  lediv12a  8827  qapne  9615  qreccl  9618  xleaddadd  9861  ixxss12  9880  ioodisj  9967  fznlem  10014  elfz0fzfz0  10099  btwnzge0  10273  mulexpzap  10533  leexp1a  10548  expnbnd  10616  hashennnuni  10730  zfz1iso  10792  seq3coll  10793  resqrexlemga  11003  sqrtsq  11024  abs3lem  11091  cau3lem  11094  minmax  11209  xrmaxiflemval  11229  xrminmax  11244  climcau  11326  summodclem2  11361  fsumrelem  11450  cvgratz  11511  mertenslemi1  11514  mertenslem2  11515  mertensabs  11516  fprodcl2lem  11584  fprodap0  11600  fprodrec  11608  fprodap0f  11615  fprodle  11619  dvdsle  11820  gcdsupex  11928  gcdsupcl  11929  bezoutlemmain  11969  bezoutlemzz  11973  dfgcd3  11981  dvdsmulgcd  11996  lcmcllem  12037  lcmgcdlem  12047  ncoprmgcdne1b  12059  qredeu  12067  oddpwdclemxy  12139  oddpwdclemdc  12143  pythagtriplem2  12236  pythagtrip  12253  pc2dvds  12299  pcz  12301  ctiunctlemfo  12410  unct  12413  mndpropd  12720  mhmeql  12753  mhmid  12855  mhmmnd  12856  mulgval  12862  reldvdsrsrg  13073  dvdsrmul1  13083  unitgrp  13097  neissex  13298  restbasg  13301  tgrest  13302  restopnb  13314  cnptopco  13355  metequiv2  13629  xmettx  13643  metcnpi3  13650  fsumcncntop  13689  elcncf2  13694  cncfmet  13712  dedekindeulemuub  13728  dedekindeulemlu  13732  dedekindicclemuub  13737  dedekindicclemlu  13741  limccnpcntop  13777  reeff1olem  13825  nninfalllem1  14380  apdiff  14419