Metamath Proof Explorer

Theorem axc5

Description: This theorem repeats sp under the name axc5 , so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 . (Contributed by NM, 18-Aug-2017) (Proof modification is discouraged.) Use sp instead. (New usage is discouraged.)

		Ref	Expression
	Assertion	axc5	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )