![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > a1d | GIF version |
Description: Deduction introducing an
embedded antecedent. (The proof was revised by
Stefan Allan, 20-Mar-2006.)
Naming convention: We often call a theorem a "deduction" and suffix its label with "d" whenever the hypotheses and conclusion are each prefixed with the same antecedent. This allows us to use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used; here φ would be replaced with a conjunction (wa 97) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 9. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 5. We usually show the theorem form without a suffix on its label (e.g. pm2.43 47 vs. pm2.43i 43 vs. pm2.43d 44). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 20-Mar-2006.) |
Ref | Expression |
---|---|
a1d.1 | ⊢ (φ → ψ) |
Ref | Expression |
---|---|
a1d | ⊢ (φ → (χ → ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a1d.1 | . 2 ⊢ (φ → ψ) | |
2 | ax-1 5 | . 2 ⊢ (ψ → (χ → ψ)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (φ → (χ → ψ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: a1ii 24 syl5com 26 mpid 37 syld 40 imim2d 48 syl5d 62 syl6d 64 impbid21d 119 imbi2d 219 adantr 261 jctild 299 jctird 300 pm3.4 316 anbi2d 437 anbi1d 438 pm2.51 580 mtod 588 pm2.76 720 condc 748 pm5.18dc 776 dcim 783 pm2.54dc 789 pm2.85dc 810 dcor 842 anordc 862 xor3dc 1275 biassdc 1283 syl6ci 1331 hbequid 1403 19.30dc 1515 equsalh 1611 equvini 1638 nfsbxyt 1816 modc 1940 euan 1953 moexexdc 1981 nebidc 2279 rgen2a 2369 ralrimivw 2387 reximdv 2414 rexlimdvw 2430 r19.32r 2451 reuind 2738 rabxmdc 3243 rexn0 3313 regexmidlem1 4218 finds1 4268 nn0suc 4270 nndceq0 4282 ssrel2 4373 poltletr 4668 fmptco 5273 nnsucsssuc 6010 fopwdom 6246 indpi 6326 nnind 7711 nn1m1nn 7713 nn1gt1 7728 nn0n0n1ge2b 8096 xrltnsym 8484 xrlttr 8486 xrltso 8487 xltnegi 8518 fzospliti 8802 elfzonlteqm1 8836 iseqfveq2 8905 bj-nn0suc0 9410 |
Copyright terms: Public domain | W3C validator |