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 1337 | . 2 | |
2 | ax-7 1337 | . 2 | |
3 | 1, 2 | impbii 117 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 98 wal 1241 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 100 ax-ia3 101 ax-7 1337 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: alrot3 1374 alrot4 1375 nfalt 1470 nfexd 1644 sbnf2 1857 sbcom2v 1861 sbalyz 1875 sbal1yz 1877 sbal2 1898 2eu4 1993 ralcomf 2471 gencbval 2602 unissb 3610 dfiin2g 3690 dftr5 3857 cotr 4706 cnvsym 4708 dffun2 4912 funcnveq 4962 fun11 4966 |
Copyright terms: Public domain | W3C validator |