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 345 con4biddc 827 jaddc 834 hbimd 1537 19.21ht 1545 nfimd 1549 19.23t 1640 spimth 1698 ssuni 3728 nnmordi 6380 omnimkv 6998 caucvgsrlemoffcau 7574 caucvgsrlemoffres 7576 facdiv 10452 facwordi 10454 bezoutlemmain 11613 bezoutlemaz 11618 bezoutlembz 11619 algcvgblem 11657 prmfac1 11757 cncfco 12674 limccnpcntop 12740 limccoap 12743 bj-rspgt 12920 |
Copyright terms: Public domain | W3C validator |