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-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: f1ocnvfvrneq 5744 fcof1o 5751 isoselem 5782 isose 5783 tposss 6205 smoiso 6261 fzssp1 9992 fzosplitsnm1 10134 fzofzp1 10152 fzostep1 10162 bcm1k 10662 climuni 11220 serf0 11279 fsumparts 11397 hashiun 11405 oddprm 12170 hmeores 12862 |
Copyright terms: Public domain | W3C validator |