Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 4syl | GIF version |
Description: Inference chaining three syllogisms. The use of this theorem is marked "discouraged" because it can cause the "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. (Contributed by BJ, 14-Jul-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
4syl.1 | ⊢ (𝜑 → 𝜓) |
4syl.2 | ⊢ (𝜓 → 𝜒) |
4syl.3 | ⊢ (𝜒 → 𝜃) |
4syl.4 | ⊢ (𝜃 → 𝜏) |
Ref | Expression |
---|---|
4syl | ⊢ (𝜑 → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4syl.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 4syl.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
3 | 4syl.3 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 1, 2, 3 | 3syl 17 | . 2 ⊢ (𝜑 → 𝜃) |
5 | 4syl.4 | . 2 ⊢ (𝜃 → 𝜏) | |
6 | 4, 5 | syl 14 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff set 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: f1ocnvfvrneq 5676 fcof1o 5683 isoselem 5714 isose 5715 tposss 6136 smoiso 6192 fzssp1 9840 fzosplitsnm1 9979 fzofzp1 9997 fzostep1 10007 bcm1k 10499 climuni 11055 serf0 11114 fsumparts 11232 hashiun 11240 hmeores 12473 |
Copyright terms: Public domain | W3C validator |