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

Metamath Proof Explorer

Theorem nfxfrd

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016)

Ref Expression
Hypotheses nfbii.1 ⊢ φ ↔ ψ
nfxfrd.2 ⊢ χ → Ⅎ x ψ
Assertion nfxfrd ⊢ χ → Ⅎ x φ

Proof

Step Hyp Ref Expression
1 nfbii.1 ⊢ φ ↔ ψ
2 nfxfrd.2 ⊢ χ → Ⅎ x ψ
3 1 nfbii ⊢ Ⅎ x φ ↔ Ⅎ x ψ
4 2 3 sylibr ⊢ χ → Ⅎ x φ