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

Metamath Proof Explorer

Theorem 19.32

Description: Theorem 19.32 of Margaris p. 90. See 19.32v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 24-Sep-2016)

		Ref	Expression
	Hypothesis	19.32.1	⊢ Ⅎ 𝑥 𝜑
	Assertion	19.32	⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∀ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		19.32.1	⊢ Ⅎ 𝑥 𝜑
2	1	nfn	⊢ Ⅎ 𝑥 ¬ 𝜑
3	2	19.21	⊢ ( ∀ 𝑥 ( ¬ 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 → ∀ 𝑥 𝜓 ) )
4		df-or	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 → 𝜓 ) )
5	4	albii	⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ∀ 𝑥 ( ¬ 𝜑 → 𝜓 ) )
6		df-or	⊢ ( ( 𝜑 ∨ ∀ 𝑥 𝜓 ) ↔ ( ¬ 𝜑 → ∀ 𝑥 𝜓 ) )
7	3 5 6	3bitr4i	⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∀ 𝑥 𝜓 ) )