Theorem dummylink 1

Description: (Note: This theorem will never appear in a completed proof and can be ignored if you are using this database to learn logic - please start with the next statement, wn 2.)

This is a technical theorem to assist proof development. It provides a temporary way to add an independent subproof to a proof under development, for later assignment to a normal proof step.

The Metamath program's Proof Assistant requires proofs to be developed backwards from the conclusion with no gaps, and it has no mechanism that lets the user to work on isolated subproofs. This theorem provides a workaround for this limitation. It can be inserted at any point in a proof to allow an independent subproof to be developed on the side, for later use as part of the final proof.

Instructions: (1) Assign this theorem to any unknown step in the proof. Typically, the last unknown step is the most convenient, since 'assign last' can be used. This step will be replicated in hypothesis dummylink.1, from where the development of the main proof can continue. (2) Develop the independent subproof backwards from hypothesis dummylink.2. If desired, use a 'let' command to pre-assign the conclusion of the independent subproof to dummylink.2. (3) Later on, use 'improve all' to assign the independent subproof to an unknown step in the main proof that matches it. (4) After the entire proof is complete, use 'minimize */n/b/e 3syl,we?,wsb' to clean up (discard) all dummylink references automatically.

This theorem was originally designed to assist importing partially completed Proof Worksheets from Mel O'Cat's mmj2 Proof Assistant GUI, but it can also be useful on its own. Interestingly, this "theorem" - or more precisely, inference - requires no axioms for its proof.

Hypotheses

Ref	Expression
dummylink.1	|- ph
dummylink.2	|- ps

Assertion

Ref	Expression
dummylink	|- ph

Proof of Theorem dummylink

Step	Hyp	Ref	Expression
1		dummylink.1	1 |- ph

Copyright terms: Public domain