Theorem simplll 522

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 108	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	ad2antrr 479	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-4l  530  f1imass  5675  tfrlem1  6205  phplem4dom  6756  phplem4on  6761  fisseneq  6820  suplub2ti  6888  omp1eomlem  6979  addcmpblnq  7175  mulcmpblnq  7176  ordpipqqs  7182  ltexnqq  7216  enq0tr  7242  addcmpblnq0  7251  mulcmpblnq0  7252  nnnq0lem1  7254  prssnql  7287  prmuloc  7374  prmuloc2  7375  mullocpr  7379  ltexprlemopu  7411  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  ltmprr  7450  archpr  7451  suplocexprlemloc  7529  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  ltsrprg  7555  srpospr  7591  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  negeu  7953  add20  8236  rimul  8347  apreap  8349  cru  8364  mulge0  8381  mulap0  8415  prodgt0  8610  ltmul12a  8618  ledivdiv  8648  lediv12a  8652  qapne  9431  qreccl  9434  xleaddadd  9670  ixxss12  9689  ioodisj  9776  fznlem  9821  elfz0fzfz0  9903  btwnzge0  10073  mulexpzap  10333  leexp1a  10348  expnbnd  10415  hashennnuni  10525  zfz1iso  10584  seq3coll  10585  resqrexlemga  10795  sqrtsq  10816  abs3lem  10883  cau3lem  10886  minmax  11001  xrmaxiflemval  11019  xrminmax  11034  climcau  11116  summodclem2  11151  fsumrelem  11240  cvgratz  11301  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  dvdsle  11542  gcdsupex  11646  gcdsupcl  11647  bezoutlemmain  11686  bezoutlemzz  11690  dfgcd3  11698  dvdsmulgcd  11713  lcmcllem  11748  lcmgcdlem  11758  ncoprmgcdne1b  11770  qredeu  11778  oddpwdclemxy  11847  oddpwdclemdc  11851  ctiunctlemfo  11952  unct  11954  neissex  12334  restbasg  12337  tgrest  12338  restopnb  12350  cnptopco  12391  metequiv2  12665  xmettx  12679  metcnpi3  12686  fsumcncntop  12725  elcncf2  12730  cncfmet  12748  dedekindeulemuub  12764  dedekindeulemlu  12768  dedekindicclemuub  12773  dedekindicclemlu  12777  limccnpcntop  12813  nninfalllemn  13202  nninfalllem1  13203