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: wi 4 |
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 326 pm5.31 346 con4biddc 843 jaddc 850 hbimd 1553 19.21ht 1561 nfimd 1565 19.23t 1657 spimth 1715 ssuni 3796 nnmordi 6465 omnimkv 7101 caucvgsrlemoffcau 7720 caucvgsrlemoffres 7722 facdiv 10623 facwordi 10625 bezoutlemmain 11897 bezoutlemaz 11902 bezoutlembz 11903 algcvgblem 11941 prmfac1 12042 cncfco 13048 limccnpcntop 13114 limccoap 13117 bj-rspgt 13431 |
Copyright terms: Public domain | W3C validator |