![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl3an | Unicode version |
Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.) |
Ref | Expression |
---|---|
syl3an.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl3an.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl3an.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl3an.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl3an |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl3an.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | syl3an.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3anim123i 1167 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | syl3an.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 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: syl2an3an 1277 funtpg 5182 ftpg 5612 eloprabga 5866 prfidisj 6823 djuenun 7085 addasspig 7162 mulasspig 7164 distrpig 7165 addcanpig 7166 mulcanpig 7167 ltapig 7170 distrnqg 7219 distrnq0 7291 cnegexlem2 7962 zletr 9127 zdivadd 9164 xaddass 9682 iooneg 9801 zltaddlt1le 9820 fzen 9854 fzaddel 9870 fzrev 9895 fzrevral2 9917 fzshftral 9919 fzosubel2 10003 fzonn0p1p1 10021 resqrexlemover 10814 fisum0diag2 11248 dvdsnegb 11546 muldvds1 11554 muldvds2 11555 dvdscmul 11556 dvdsmulc 11557 dvds2add 11563 dvds2sub 11564 dvdstr 11566 addmodlteqALT 11593 divalgb 11658 ndvdsadd 11664 absmulgcd 11741 rpmulgcd 11750 cncongr2 11821 hashdvds 11933 |
Copyright terms: Public domain | W3C validator |