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

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 (φ → (ψ χ))
Assertion
Ref Expression
simpld (φψ)

Proof of Theorem simpld
StepHypRef Expression
1 simpld.1 . 2 (φ → (ψ χ))
2 simpl 443 . 2 ((ψ χ) → ψ)
31, 2syl 15 1 (φψ)
 Colors of variables: wff setvar class 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  3440  preaddccan2  4455  leltfintr  4458  ltfintri  4466  ncfindi  4475  ncfinsn  4476  ncfineleq  4477  tfincl  4492  ncfintfin  4495  tfinltfinlem1  4500  tfinltfin  4501  evenoddnnnul  4514  evenodddisj  4516  eventfin  4517  oddtfin  4518  sfinltfin  4535  1cvsfin  4542  vfintle  4546  vfin1cltv  4547  vfinncvntnn  4548  vfinspsslem1  4550  vfinncsp  4554  brreldmex  4690  epelc  4765  opeliunxp2  4822  br1st  4858  br2nd  4859  brswap2  4860  brco  4883  imasn  5018  fun11iun  5305  fvprc  5325  ndmovordi  5621  elovex1  5649  elfix  5787  pmfun  6015  ncseqnc  6128  elce  6175  nchoicelem19  6307
 Copyright terms: Public domain W3C validator