Metamath Proof Explorer


Theorem dral1

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 . Use the weaker dral1v if possible. (Contributed by NM, 24-Nov-1994) Remove dependency on ax-11 . (Revised by Wolf Lammen, 6-Sep-2018) (New usage is discouraged.)

Ref Expression
Hypothesis dral1.1 xx=yφψ
Assertion dral1 xx=yxφyψ

Proof

Step Hyp Ref Expression
1 dral1.1 xx=yφψ
2 nfa1 xxx=y
3 2 1 albid xx=yxφxψ
4 axc11 xx=yxψyψ
5 axc11r xx=yyψxψ
6 4 5 impbid xx=yxψyψ
7 3 6 bitrd xx=yxφyψ