| Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HOLE Home > Th. List > trud | Unicode version | ||
| Description: Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.) |
| Ref | Expression |
|---|---|
| ax-trud.1 |
|
| Ref | Expression |
|---|---|
| trud |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-trud.1 |
. 2
| |
| 2 | 1 | ax-trud 26 |
1
|
| Colors of variables: type var term |
| Syntax hints: |
| This theorem was proved from axioms: ax-trud 26 |
| This theorem is referenced by: trul 39 hbov 111 ax4g 149 dfan2 154 hbct 155 axun 222 |
| Copyright terms: Public domain | W3C validator |