![]() |
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 5782 fcof1o 5789 isoselem 5820 isose 5821 tposss 6246 smoiso 6302 fzssp1 10066 fzosplitsnm1 10208 fzofzp1 10226 fzostep1 10236 bcm1k 10739 climuni 11300 serf0 11359 fsumparts 11477 hashiun 11485 oddprm 12258 hmeores 13785 |
Copyright terms: Public domain | W3C validator |