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 327 | . 2 |
3 | 2 | imp 123 | 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: xoranor 1355 nfan1 1543 sbcof2 1782 difin 3313 difrab 3350 opthreg 4471 wessep 4492 fvelimab 5477 elfvmptrab 5516 dffo4 5568 dffo5 5569 ltaddpr 7405 recgt1i 8656 elnnnn0c 9022 elnnz1 9077 recnz 9144 eluz2b2 9397 elfzp12 9879 cos01gt0 11469 oddnn02np1 11577 |
Copyright terms: Public domain | W3C validator |