Theorem idi 1

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.)

Hypothesis

Ref	Expression
idi.1	⊢ 𝜑

Assertion

Ref	Expression
idi	⊢ 𝜑

Proof of Theorem idi

Step	Hyp	Ref	Expression
1		idi.1	1 ⊢ 𝜑

This theorem is referenced by:  madjusmdetlem2  31778  imo72b2lem0  41776  ssmapsn  42756  fprodcnlem  43140  limsupvaluz2  43279  dvmptfprod  43486  dvnprodlem1  43487  sge0f1o  43920  smfinfmpt  44352  rngcifuestrc  45555