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 7412 recgt1i 8663 elnnnn0c 9029 elnnz1 9084 recnz 9151 eluz2b2 9404 elfzp12 9886 cos01gt0 11476 oddnn02np1 11584 |
Copyright terms: Public domain | W3C validator |