| Description: (Note: This
inference rule and the next one, a1ii 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 inference says "if 𝜑 is true then 𝜑 is true". This
inference requires no axioms for its proof, and 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. You can remove this using the metamath-exe (Metamath
program) Proof Assistant using the "MM-PA> MINIMIZE_WITH *"
command.
This is the inference associated with id 22, hence
its name.
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is
discouraged.) |
