Theorem hbanOLD

Description: Obsolete version of hban as of 22-Oct-2026. (Contributed by NM, 14-May-1993) (Proof shortened by Wolf Lammen, 2-Jan-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hbOLD.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	hbOLD.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
Assertion	hbanOLD	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		hbOLD.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		hbOLD.2	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
3	1	nf5i	⊢ Ⅎ 𝑥 𝜑
4	2	nf5i	⊢ Ⅎ 𝑥 𝜓
5	3 4	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝜓 )
6	5	nf5ri	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥 ( 𝜑 ∧ 𝜓 ) )