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 1166 | . 2 |
5 | syl3an.4 | . 2 | |
6 | 4, 5 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 962 |
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 964 |
This theorem is referenced by: syl2an3an 1276 funtpg 5169 ftpg 5597 eloprabga 5851 prfidisj 6808 djuenun 7061 addasspig 7131 mulasspig 7133 distrpig 7134 addcanpig 7135 mulcanpig 7136 ltapig 7139 distrnqg 7188 distrnq0 7260 cnegexlem2 7931 zletr 9096 zdivadd 9133 xaddass 9645 iooneg 9764 zltaddlt1le 9782 fzen 9816 fzaddel 9832 fzrev 9857 fzrevral2 9879 fzshftral 9881 fzosubel2 9965 fzonn0p1p1 9983 resqrexlemover 10775 fisum0diag2 11209 dvdsnegb 11499 muldvds1 11507 muldvds2 11508 dvdscmul 11509 dvdsmulc 11510 dvds2add 11516 dvds2sub 11517 dvdstr 11519 addmodlteqALT 11546 divalgb 11611 ndvdsadd 11617 absmulgcd 11694 rpmulgcd 11703 cncongr2 11774 hashdvds 11886 |
Copyright terms: Public domain | W3C validator |