Metamath Proof Explorer


Theorem sbtd

Description: A true statement is true upon substitution (deduction). A similar proof is possible for icht . (Contributed by SN, 4-May-2024)

Ref Expression
Hypothesis sbtd.1
|- ( ph -> ps )
Assertion sbtd
|- ( ph -> [ t / x ] ps )

Proof

Step Hyp Ref Expression
1 sbtd.1
 |-  ( ph -> ps )
2 1 alrimiv
 |-  ( ph -> A. x ps )
3 stdpc4
 |-  ( A. x ps -> [ t / x ] ps )
4 2 3 syl
 |-  ( ph -> [ t / x ] ps )