Metamath Proof Explorer


Theorem dral1-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 dral1 using ax-c11 . (Contributed by NM, 24-Nov-1994) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dral1-o.1 x x = y φ ψ
2 hbae-o x x = y x x x = y
3 1 biimpd x x = y φ ψ
4 2 3 alimdh x x = y x φ x ψ
5 ax-c11 x x = y x ψ y ψ
6 4 5 syld x x = y x φ y ψ
7 hbae-o x x = y y x x = y
8 1 biimprd x x = y ψ φ
9 7 8 alimdh x x = y y ψ y φ
10 ax-c11 y y = x y φ x φ
11 10 aecoms-o x x = y y φ x φ
12 9 11 syld x x = y y ψ x φ
13 6 12 impbid x x = y x φ y ψ