Theorem nfan1OLDOLD 2184

Description: Obsolete version of nfan1 2183 as of 7-Jul-2022. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1828 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
nfim1.1	⊢ Ⅎ𝑥𝜑
nfim1.2	⊢ (𝜑 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfan1OLDOLD	⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Proof of Theorem nfan1OLDOLD

Step	Hyp	Ref	Expression
1		df-an 387	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2		nfim1.1	. . . 4 ⊢ Ⅎ𝑥𝜑
3		nfim1.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4		nfnt 1901	. . . . 5 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
6	2, 5	nfim1 2182	. . 3 ⊢ Ⅎ𝑥(𝜑 → ¬ 𝜓)
7	6	nfn 1902	. 2 ⊢ Ⅎ𝑥 ¬ (𝜑 → ¬ 𝜓)
8	1, 7	nfxfr 1897	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386  Ⅎwnf 1827

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-12 2163

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828

This theorem is referenced by: (None)