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 5651 fcof1o 5658 isoselem 5689 isose 5690 tposss 6111 smoiso 6167 fzssp1 9815 fzosplitsnm1 9954 fzofzp1 9972 fzostep1 9982 bcm1k 10474 climuni 11030 serf0 11089 fsumparts 11207 hashiun 11215 hmeores 12411 |
Copyright terms: Public domain | W3C validator |