![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: f1ocnvfvrneq 5561 fcof1o 5568 isoselem 5599 isose 5600 tposss 6011 smoiso 6067 fzssp1 9481 fzosplitsnm1 9620 fzofzp1 9638 fzostep1 9648 bcm1k 10168 climuni 10681 serf0 10741 fsumparts 10864 hashiun 10872 |
Copyright terms: Public domain | W3C validator |