Metamath Proof Explorer


Theorem fvmptd4

Description: Deduction version of fvmpt (where the substitution hypothesis does not have the antecedent ph ). (Contributed by SN, 26-Jul-2024)

Ref Expression
Hypotheses fvmptd4.1 ( 𝑥 = 𝐴𝐵 = 𝐶 )
fvmptd4.2 ( 𝜑𝐹 = ( 𝑥𝐷𝐵 ) )
fvmptd4.3 ( 𝜑𝐴𝐷 )
fvmptd4.4 ( 𝜑𝐶𝑉 )
Assertion fvmptd4 ( 𝜑 → ( 𝐹𝐴 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 fvmptd4.1 ( 𝑥 = 𝐴𝐵 = 𝐶 )
2 fvmptd4.2 ( 𝜑𝐹 = ( 𝑥𝐷𝐵 ) )
3 fvmptd4.3 ( 𝜑𝐴𝐷 )
4 fvmptd4.4 ( 𝜑𝐶𝑉 )
5 1 adantl ( ( 𝜑𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
6 2 5 3 4 fvmptd ( 𝜑 → ( 𝐹𝐴 ) = 𝐶 )