![]() |
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 102) 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 52 vs. pm2.43i 48 vs. pm2.43d 49). (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: 2a1d 23 a1i13 24 2a1i 27 syl5com 29 mpid 41 syld 44 imim2d 53 syl5d 67 syl6d 69 impbid21d 126 imbi2d 228 adantr 270 jctild 309 jctird 310 pm3.4 326 anbi2d 452 anbi1d 453 pm2.51 614 mtod 622 pm2.76 755 condc 783 pm5.18dc 811 dcim 818 pm2.54dc 824 pm2.85dc 845 dcor 877 anordc 898 xor3dc 1319 biassdc 1327 syl6ci 1375 hbequid 1447 19.30dc 1559 equsalh 1656 equvini 1683 nfsbxyt 1862 modc 1986 euan 1999 moexexdc 2027 nebidc 2329 rgen2a 2423 ralrimivw 2441 reximdv 2468 rexlimdvw 2486 r19.32r 2507 reuind 2806 rabxmdc 3297 rexn0 3361 regexmidlem1 4311 finds1 4379 nn0suc 4381 nndceq0 4393 ssrel2 4485 poltletr 4786 fmptco 5405 nnsucsssuc 6184 map1 6458 1domsn 6464 fopwdom 6481 mapxpen 6493 fidifsnen 6515 eldju2ndl 6669 eldju2ndr 6670 finomni 6700 fodjuomnilemdc 6703 pr2ne 6722 exmidfodomrlemim 6729 indpi 6803 nnindnn 7330 nnind 8331 nn1m1nn 8333 nn1gt1 8348 nn0n0n1ge2b 8721 xrltnsym 9157 xrlttr 9159 xrltso 9160 xltnegi 9191 fzospliti 9475 elfzonlteqm1 9509 qbtwnxr 9557 modfzo0difsn 9690 monoord 9769 rexuz3 10249 rexanuz2 10250 dvdsle 10624 dvdsabseq 10627 nno 10685 nn0seqcvgd 10802 lcmdvds 10840 divgcdcoprm0 10862 exprmfct 10898 rpexp1i 10912 phibndlem 10971 bj-nn0suc0 11187 |
Copyright terms: Public domain | W3C validator |