![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imdistani | Unicode version |
Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
imdistani.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imdistani |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imdistani.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anc2li 329 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 124 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: syldanl 449 xoranor 1377 nfan1 1564 sbcof2 1810 difin 3372 difrab 3409 opthreg 4552 wessep 4574 fvelimab 5568 elfvmptrab 5607 dffo4 5660 dffo5 5661 ltaddpr 7584 recgt1i 8841 elnnnn0c 9207 elnnz1 9262 recnz 9332 eluz2b2 9589 elfzp12 10082 cos01gt0 11751 oddnn02np1 11865 reumodprminv 12233 sgrpidmndm 12710 bj-charfundc 14213 |
Copyright terms: Public domain | W3C validator |