![]() |
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 3391 reupick 3419 issod 4319 poxp 6232 smores2 6294 smoiun 6301 mapxpen 6847 f1dmvrnfibi 6942 recexprlemm 7622 ltleletr 8037 fzind 9366 iccid 9923 ssfzo12bi 10222 dvdsabseq 11847 divalgb 11924 cncongr1 12097 difsqpwdvds 12331 txlm 13672 blsscls2 13886 metcnpi3 13910 |
Copyright terms: Public domain | W3C validator |