This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dral2

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 . Usage of albidv is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005) Allow a shortening of dral1 . (Revised by Wolf Lammen, 4-Mar-2018) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	dral1.1	\|- ( A. x x = y -> ( ph <-> ps ) )
	Assertion	dral2	\|- ( A. x x = y -> ( A. z ph <-> A. z ps ) )

Proof

Step	Hyp	Ref	Expression
1		dral1.1	\|- ( A. x x = y -> ( ph <-> ps ) )
2		nfae	\|- F/ z A. x x = y
3	2 1	albid	\|- ( A. x x = y -> ( A. z ph <-> A. z ps ) )