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
|- ( ph -> ( ps <-> ch ) )
Assertion bj-ax12wlem
|- ( ph -> ( ps -> A. x ( ph -> ps ) ) )

Proof

Step Hyp Ref Expression
1 bj-ax12wlem.1
 |-  ( ph -> ( ps <-> ch ) )
2 ax-5
 |-  ( ch -> A. x ch )
3 1 2 bj-ax12i
 |-  ( ph -> ( ps -> A. x ( ph -> ps ) ) )