New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > syld | GIF version |
Description: Syllogism deduction.
(Contributed by NM, 5-Aug-1993.) (Proof shortened
by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Notice that syld 40 has the same form as syl 15 with φ added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace φ with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 19 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible. |
Ref | Expression |
---|---|
syld.1 | ⊢ (φ → (ψ → χ)) |
syld.2 | ⊢ (φ → (χ → θ)) |
Ref | Expression |
---|---|
syld | ⊢ (φ → (ψ → θ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syld.1 | . 2 ⊢ (φ → (ψ → χ)) | |
2 | syld.2 | . . 3 ⊢ (φ → (χ → θ)) | |
3 | 2 | a1d 22 | . 2 ⊢ (φ → (ψ → (χ → θ))) |
4 | 1, 3 | mpdd 36 | 1 ⊢ (φ → (ψ → θ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: 3syld 51 sylsyld 52 nsyld 132 pm2.61d 150 sylibd 205 sylbid 206 sylibrd 225 sylbird 226 syland 467 alrimdd 1768 dvelimv 1939 ax10lem6 1943 dral1 1965 cbv1h 1978 sbied 2036 sbequi 2059 dral1-o 2154 ax11indalem 2197 ax11inda2ALT 2198 pwadjoin 4119 nnsucelr 4428 nndisjeq 4429 lenltfin 4469 ncfinlower 4483 tfin11 4493 evenodddisj 4516 nnadjoin 4520 nnpweq 4523 tfinnn 4534 sfinltfin 4535 vfintle 4546 vfinspsslem1 4550 eqfnfv 5392 ncssfin 6151 addccan2nc 6265 spacind 6287 nchoicelem9 6297 nchoicelem12 6300 nchoicelem17 6305 nchoicelem19 6307 fnfreclem3 6319 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |