Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 4syl | Unicode 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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: f1ocnvfvrneq 5422 fcof1o 5429 isoselem 5459 isose 5460 tposss 5861 smoiso 5917 fzssp1 8930 fzosplitsnm1 9065 fzofzp1 9083 fzostep1 9093 climuni 9814 serif0 9871 |
Copyright terms: Public domain | W3C validator |