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 ⊢ φ → Ⅎ _ x A
nfovd.3 ⊢ φ → Ⅎ _ x F
nfovd.4 ⊢ φ → Ⅎ _ x B
Assertion nfovd ⊢ φ → Ⅎ _ x A F B

Proof

Step Hyp Ref Expression
1 nfovd.2 ⊢ φ → Ⅎ _ x A
2 nfovd.3 ⊢ φ → Ⅎ _ x F
3 nfovd.4 ⊢ φ → Ⅎ _ x B
4 df-ov ⊢ A F B = F ⁡ A B
5 1 3 nfopd ⊢ φ → Ⅎ _ x A B
6 2 5 nffvd ⊢ φ → Ⅎ _ x F ⁡ A B
7 4 6 nfcxfrd ⊢ φ → Ⅎ _ x A F B