![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alcom | Unicode version |
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-7 1382 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-7 1382 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 124 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 105 ax-ia3 106 ax-7 1382 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: alrot3 1419 alrot4 1420 nfalt 1515 nfexd 1691 sbnf2 1905 sbcom2v 1909 sbalyz 1923 sbal1yz 1925 sbal2 1946 2eu4 2041 ralcomf 2528 gencbval 2667 unissb 3683 dfiin2g 3763 dftr5 3939 cotr 4813 cnvsym 4815 dffun2 5025 funcnveq 5077 fun11 5081 |
Copyright terms: Public domain | W3C validator |