![]() |
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 1448 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-7 1448 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 126 |
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-ia2 107 ax-ia3 108 ax-7 1448 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: alrot3 1485 alrot4 1486 nfalt 1578 nfexd 1761 sbnf2 1981 sbcom2v 1985 sbalyz 1999 sbal1yz 2001 sbal2 2020 2eu4 2119 ralcomf 2638 gencbval 2787 unissb 3841 dfiin2g 3921 dftr5 4106 cotr 5012 cnvsym 5014 dffun2 5228 funcnveq 5281 fun11 5285 |
Copyright terms: Public domain | W3C validator |