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  5914  tfrlem1  6473  phplem4dom  7047  phplem4on  7053  fisseneq  7126  suplub2ti  7199  omp1eomlem  7292  nnnninfeq  7326  nninfisol  7331  exmidontriim  7439  addcmpblnq  7586  mulcmpblnq  7587  ordpipqqs  7593  ltexnqq  7627  enq0tr  7653  addcmpblnq0  7662  mulcmpblnq0  7663  nnnq0lem1  7665  prssnql  7698  prmuloc  7785  prmuloc2  7786  mullocpr  7790  ltexprlemopu  7822  ltexprlemrl  7829  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  ltmprr  7861  archpr  7862  suplocexprlemloc  7940  addcmpblnr  7958  mulcmpblnrlemg  7959  mulcmpblnr  7960  ltsrprg  7966  srpospr  8002  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  negeu  8369  add20  8653  rimul  8764  apreap  8766  cru  8781  mulge0  8798  mulap0  8833  prodgt0  9031  ltmul12a  9039  ledivdiv  9069  lediv12a  9073  qapne  9872  qreccl  9875  xleaddadd  10121  ixxss12  10140  ioodisj  10227  fznlem  10275  elfz0fzfz0  10360  btwnzge0  10559  seqf1og  10782  mulexpzap  10840  leexp1a  10855  expnbnd  10924  hashennnuni  11040  zfz1iso  11104  seq3coll  11105  swrdswrdlem  11284  pfxccatin12lem3  11312  resqrexlemga  11583  sqrtsq  11604  abs3lem  11671  cau3lem  11674  minmax  11790  xrmaxiflemval  11810  xrminmax  11825  climcau  11907  summodclem2  11942  fsumrelem  12031  cvgratz  12092  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  fprodcl2lem  12165  fprodap0  12181  fprodrec  12189  fprodap0f  12196  fprodle  12200  dvdsle  12404  bitsfzo  12515  bezoutlemmain  12568  bezoutlemzz  12572  dfgcd3  12580  dvdsmulgcd  12595  lcmcllem  12638  lcmgcdlem  12648  ncoprmgcdne1b  12660  qredeu  12668  oddpwdclemxy  12740  oddpwdclemdc  12744  pythagtriplem2  12838  pythagtrip  12855  pc2dvds  12902  pcz  12904  ctiunctlemfo  13059  unct  13062  sgrppropd  13495  mndpropd  13522  mhmeql  13574  mhmid  13701  mhmmnd  13702  mulgval  13708  issubg4m  13779  imasabl  13922  gsumfzconst  13927  dvdsrmul1  14115  unitgrp  14129  neissex  14888  restbasg  14891  tgrest  14892  restopnb  14904  cnptopco  14945  metequiv2  15219  xmettx  15233  metcnpi3  15240  mpomulcn  15289  fsumcncntop  15290  elcncf2  15297  cncfmet  15315  dedekindeulemuub  15340  dedekindeulemlu  15344  dedekindicclemuub  15349  dedekindicclemlu  15353  limccnpcntop  15398  dvmptfsum  15448  reeff1olem  15494  lgsquad3  15812  clwwlkccatlem  16250  nninfalllem1  16610  nninfnfiinf  16625  apdiff  16652