Metamath Proof Explorer


Theorem sbhypf

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004) (Proof shortened by Wolf Lammen, 25-Jan-2025)

Ref Expression
Hypotheses sbhypf.1 x ψ
sbhypf.2 x = A φ ψ
Assertion sbhypf y = A y x φ ψ

Proof

Step Hyp Ref Expression
1 sbhypf.1 x ψ
2 sbhypf.2 x = A φ ψ
3 2 sbimi y x x = A y x φ ψ
4 eqsb1 y x x = A y = A
5 1 sbf y x ψ ψ
6 5 sblbis y x φ ψ y x φ ψ
7 3 4 6 3imtr3i y = A y x φ ψ