![]() |
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 5800 fcof1o 5807 isoselem 5838 isose 5839 tposss 6266 smoiso 6322 fzssp1 10092 fzosplitsnm1 10234 fzofzp1 10252 fzostep1 10262 bcm1k 10767 climuni 11328 serf0 11387 fsumparts 11505 hashiun 11513 oddprm 12286 hmeores 14252 |
Copyright terms: Public domain | W3C validator |