![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imim2d | Unicode version |
Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imim2d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imim2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim2d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1d 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | a2d 26 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: imim2 55 embantd 56 imim12d 74 anc2r 328 pm5.31 348 con4biddc 858 jaddc 865 hbimd 1584 19.21ht 1592 nfimd 1596 19.23t 1688 spimth 1746 ssuni 3849 nnmordi 6545 omnimkv 7189 caucvgsrlemoffcau 7832 caucvgsrlemoffres 7834 facdiv 10759 facwordi 10761 bezoutlemmain 12040 bezoutlemaz 12045 bezoutlembz 12046 algcvgblem 12092 prmfac1 12195 infpnlem1 12402 cncfco 14563 limccnpcntop 14629 limccoap 14632 bj-rspgt 15024 |
Copyright terms: Public domain | W3C validator |