This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfovd

Description: Deduction version of bound-variable hypothesis builder nfov . (Contributed by NM, 13-Dec-2005) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	nfovd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfovd.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
	nfovd.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion	nfovd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐴 𝐹 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nfovd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfovd.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
3		nfovd.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
4		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
5	1 3	nfopd	⊢ ( 𝜑 → Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩ )
6	2 5	nffvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
7	4 6	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐴 𝐹 𝐵 ) )