New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simpld | GIF version |
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.) |
Ref | Expression |
---|---|
simpld.1 | ⊢ (φ → (ψ ∧ χ)) |
Ref | Expression |
---|---|
simpld | ⊢ (φ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpld.1 | . 2 ⊢ (φ → (ψ ∧ χ)) | |
2 | simpl 443 | . 2 ⊢ ((ψ ∧ χ) → ψ) | |
3 | 1, 2 | syl 15 | 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: 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 |