Theorem simprd 449

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.) A translation of natural deduction rule ∧ ER (∧ elimination right), see natded in set.mm. (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
simprd.1	⊢ (φ → (ψ ∧ χ))

Assertion

Ref	Expression
simprd	⊢ (φ → χ)

Proof of Theorem simprd

Step	Hyp	Ref	Expression
1		simprd.1	. . 3 ⊢ (φ → (ψ ∧ χ))
2	1	ancomd 438	. 2 ⊢ (φ → (χ ∧ ψ))
3	2	simpld 445	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ∧ wa 358

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

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

This theorem is referenced by:  simprbi  450  simplbda  607  simp2  956  simp3  957  nic-mp  1436  nic-mpALT  1437  unssbd  3441  ncfindi  4475  ncfinsn  4476  ncfineleq  4477  ncfintfin  4495  tfinltfinlem1  4500  evennnul  4508  oddnnul  4509  1cvsfin  4542  vfintle  4546  vfin1cltv  4547  vfinncvntnn  4548  vfinspsslem1  4550  vfinncsp  4554  brrelrnex  4691  elima  4754  vtoclr  4816  brco  4883  brres  4949  elimasn  5019  feu  5242  fun11iun  5305  fv3  5341  opbr1st  5501  opbr2nd  5502  ndmovord  5620  caovmo  5645  elovex2  5650  brfns  5833  fnfullfunlem1  5856  frds  5935  brltc  6114  eqncg  6126  nmembers1lem3  6270  spacind  6287  nchoicelem3  6291  nchoicelem5  6293  nchoice  6308