Metamath Proof Explorer

Theorem dral2-o

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Version of dral2 using ax-c11 . (Contributed by NM, 27-Feb-2005) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis dral2-o.1 x x = y φ ψ
Assertion dral2-o x x = y z φ z ψ


Step Hyp Ref Expression
1 dral2-o.1 x x = y φ ψ
2 hbae-o x x = y z x x = y
3 2 1 albidh x x = y z φ z ψ