Metamath Proof Explorer


Theorem bj-ax12wlem

Description: A lemma used to prove a weak version of the axiom of substitution ax-12 . (Temporary comment: The general statement that ax12wlem proves.) (Contributed by BJ, 20-Mar-2020)

Ref Expression
Hypothesis bj-ax12wlem.1 φψχ
Assertion bj-ax12wlem φψxφψ

Proof

Step Hyp Ref Expression
1 bj-ax12wlem.1 φψχ
2 ax-5 χxχ
3 1 2 bj-ax12i φψxφψ