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 φ ψ
Assertion sbtd φ t x ψ

Proof

Step Hyp Ref Expression
1 sbtd.1 φ ψ
2 1 alrimiv φ x ψ
3 stdpc4 x ψ t x ψ
4 2 3 syl φ t x ψ