MPE Home Metamath Proof Explorer < Wrap   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1ii Structured version   Visualization version   GIF version

Theorem a1ii 1
Description: (Note: This inference rule and the next one, idi 2, will normally never appear in a completed proof. They can be ignored if you are using this database to assist learning logic - please start with the statement wn 3 instead.)

This is a technical inference 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 inference 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 inference 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 a1ii.1, from where the development of the main proof can continue. (2) Develop the independent subproof backwards from hypothesis a1ii.2. If desired, use a 'let' command to pre-assign the conclusion of the independent subproof to a1ii.2. (3) After the independent subproof is complete, use 'improve all' to assign it automatically to an unknown step in the main proof that matches it. (4) After the entire proof is complete, use 'minimize *' to clean up (discard) all a1ii 1 references automatically.

This inference was originally designed to assist importing partially completed Proof Worksheets from the mmj2 Proof Assistant GUI, but it can also be useful on its own. Interestingly, no axioms are required for its proof. It is the inference associated with a1i 11. (Contributed by NM, 7-Feb-2006.)

Ref Expression
a1ii.1 𝜑
a1ii.2 𝜓
Ref Expression
a1ii 𝜑

Proof of Theorem a1ii
StepHypRef Expression
1 a1ii.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator