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: wi 4 w3a 963 |
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 1280 funtpg 5223 ftpg 5653 eloprabga 5910 prfidisj 6873 djuenun 7149 addasspig 7252 mulasspig 7254 distrpig 7255 addcanpig 7256 mulcanpig 7257 ltapig 7260 distrnqg 7309 distrnq0 7381 cnegexlem2 8055 zletr 9221 zdivadd 9258 xaddass 9779 iooneg 9898 zltaddlt1le 9917 fzen 9951 fzaddel 9967 fzrev 9992 fzrevral2 10014 fzshftral 10016 fzosubel2 10103 fzonn0p1p1 10121 resqrexlemover 10921 fisum0diag2 11355 dvdsnegb 11715 muldvds1 11723 muldvds2 11724 dvdscmul 11725 dvdsmulc 11726 dvds2add 11732 dvds2sub 11733 dvdstr 11735 addmodlteqALT 11763 divalgb 11828 ndvdsadd 11834 absmulgcd 11916 rpmulgcd 11925 cncongr2 11996 hashdvds 12111 pythagtriplem1 12155 |
Copyright terms: Public domain | W3C validator |