Metamath Proof Explorer


Theorem gm-sbtru

Description: Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019)

Ref Expression
Hypothesis gm-sbtru.1 A V
Assertion gm-sbtru [˙A / x]˙

Proof

Step Hyp Ref Expression
1 gm-sbtru.1 A V
2 sbcg A V [˙A / x]˙
3 1 2 ax-mp [˙A / x]˙