New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  simprd GIF version

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
StepHypRef Expression
1 simprd.1 . . 3 (φ → (ψ χ))
21ancomd 438 . 2 (φ → (χ ψ))
32simpld 445 1 (φχ)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator