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 5683 fcof1o 5690 isoselem 5721 isose 5722 tposss 6143 smoiso 6199 fzssp1 9847 fzosplitsnm1 9986 fzofzp1 10004 fzostep1 10014 bcm1k 10506 climuni 11062 serf0 11121 fsumparts 11239 hashiun 11247 hmeores 12484 |
Copyright terms: Public domain | W3C validator |