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: 2a1i 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 581 mtod 589 pm2.76 721 condc 749 pm5.18dc 777 dcim 784 pm2.54dc 790 pm2.85dc 811 dcor 843 anordc 863 xor3dc 1278 biassdc 1286 syl6ci 1334 hbequid 1406 19.30dc 1518 equsalh 1614 equvini 1641 nfsbxyt 1819 modc 1943 euan 1956 moexexdc 1984 nebidc 2285 rgen2a 2375 ralrimivw 2393 reximdv 2420 rexlimdvw 2436 r19.32r 2457 reuind 2744 rabxmdc 3249 rexn0 3319 regexmidlem1 4258 finds1 4325 nn0suc 4327 nndceq0 4339 ssrel2 4430 poltletr 4725 fmptco 5330 nnsucsssuc 6071 fopwdom 6310 fidifsnen 6331 indpi 6440 nnindnn 6967 nnind 7930 nn1m1nn 7932 nn1gt1 7947 nn0n0n1ge2b 8320 xrltnsym 8714 xrlttr 8716 xrltso 8717 xltnegi 8748 fzospliti 9032 elfzonlteqm1 9066 iseqfveq2 9228 iseqshft2 9232 monoord 9235 iseqsplit 9238 rexuz3 9588 rexanuz2 9589 nn0seqcvgd 9880 bj-nn0suc0 10075 |
Copyright terms: Public domain | W3C validator |