Theorem idi

Description: (_Note_: This inference rule and the next one, a1ii , 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 instead.)

This inference says "if ph is true then ph 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 , hence its name. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	idi.1	|- ph
Assertion	idi	|- ph

Proof

Step	Hyp	Ref	Expression
1		idi.1	|- ph