Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > idi | GIF version |
Description: Inference form of id 19. This inference rule, which requires no axioms for its proof, is useful as a copy-paste mechanism during proof development in mmj2. It is normally not referenced in the final version of a proof, since it is always redundant and can be removed using the 'minimize *' command in the metamath program's Proof Assistant. (Contributed by Alan Sare, 31-Dec-2011.) |
Ref | Expression |
---|---|
idi.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
idi | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idi.1 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |