![]() |
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: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: f1ocnvfvrneq 5783 fcof1o 5790 isoselem 5821 isose 5822 tposss 6247 smoiso 6303 fzssp1 10067 fzosplitsnm1 10209 fzofzp1 10227 fzostep1 10237 bcm1k 10740 climuni 11301 serf0 11360 fsumparts 11478 hashiun 11486 oddprm 12259 hmeores 13818 |
Copyright terms: Public domain | W3C validator |