Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > expcomd | Unicode version |
Description: Deduction form of expcom 115. (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 256 | . 2 |
3 | 2 | com23 78 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: simplbi2comg 1419 2moswapdc 2089 indifdir 3332 reupick 3360 issod 4241 poxp 6129 smores2 6191 smoiun 6198 mapxpen 6742 f1dmvrnfibi 6832 recexprlemm 7432 ltleletr 7846 fzind 9166 iccid 9708 ssfzo12bi 10002 dvdsabseq 11545 divalgb 11622 cncongr1 11784 txlm 12448 blsscls2 12662 metcnpi3 12686 |
Copyright terms: Public domain | W3C validator |