Metamath Proof Explorer


Theorem nfan1

Description: A closed form of nfan . (Contributed by Mario Carneiro, 3-Oct-2016) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021) (Proof shortened by Wolf Lammen, 7-Jul-2022)

Ref Expression
Hypotheses nfim1.1 𝑥 𝜑
nfim1.2 ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion nfan1 𝑥 ( 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 nfim1.1 𝑥 𝜑
2 nfim1.2 ( 𝜑 → Ⅎ 𝑥 𝜓 )
3 df-an ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑 → ¬ 𝜓 ) )
4 2 nfnd ( 𝜑 → Ⅎ 𝑥 ¬ 𝜓 )
5 1 4 nfim1 𝑥 ( 𝜑 → ¬ 𝜓 )
6 5 nfn 𝑥 ¬ ( 𝜑 → ¬ 𝜓 )
7 3 6 nfxfr 𝑥 ( 𝜑𝜓 )