![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expcomd | Unicode version |
Description: Deduction form of expcom 116. (Contributed by Alan Sare, 22-Jul-2012.) |
Ref | Expression |
---|---|
expcomd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
expcomd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expcomd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | expd 258 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | com23 78 |
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-ia3 108 |
This theorem is referenced by: simplbi2comg 1443 2moswapdc 2116 indifdir 3392 reupick 3420 issod 4320 poxp 6233 smores2 6295 smoiun 6302 mapxpen 6848 f1dmvrnfibi 6943 recexprlemm 7623 ltleletr 8039 fzind 9368 iccid 9925 ssfzo12bi 10225 dvdsabseq 11853 divalgb 11930 cncongr1 12103 difsqpwdvds 12337 txlm 13782 blsscls2 13996 metcnpi3 14020 |
Copyright terms: Public domain | W3C validator |