Theorem simpld 445

Description: Deduction eliminating a conjunct. A translation of natural deduction rule /\ EL (/\ elimination left), see natded in set.mm. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
simpld.1	|- (ph -> (ps /\ ch))

Assertion

Ref	Expression
simpld	|- (ph -> ps)

Proof of Theorem simpld

Step	Hyp	Ref	Expression
1		simpld.1	. 2 |- (ph -> (ps /\ ch))
2		simpl 443	. 2 |- ((ps /\ ch) -> ps)
3	1, 2	syl 15	1 |- (ph -> ps)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  simplbi  446  simprd  449  simprbda  606  simp1  955  unssad  3441  preaddccan2  4456  leltfintr  4459  ltfintri  4467  ncfindi  4476  ncfinsn  4477  ncfineleq  4478  tfincl  4493  ncfintfin  4496  tfinltfinlem1  4501  tfinltfin  4502  evenoddnnnul  4515  evenodddisj  4517  eventfin  4518  oddtfin  4519  sfinltfin  4536  1cvsfin  4543  vfintle  4547  vfin1cltv  4548  vfinncvntnn  4549  vfinspsslem1  4551  vfinncsp  4555  brreldmex  4691  epelc  4766  opeliunxp2  4823  br1st  4859  br2nd  4860  brswap2  4861  brco  4884  imasn  5019  fun11iun  5306  fvprc  5326  ndmovordi  5622  elovex1  5650  elfix  5788  pmfun  6016  ncseqnc  6129  elce  6176  nchoicelem19  6308