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

Metamath Proof Explorer

Theorem 19.31v

Description: Version of 19.31 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020)

Ref Expression
Assertion 19.31v ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∨ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.32v ⊢ ( ∀ 𝑥 ( 𝜓 ∨ 𝜑 ) ↔ ( 𝜓 ∨ ∀ 𝑥 𝜑 ) )
2 orcom ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜓 ∨ 𝜑 ) )
3 2 albii ⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ∀ 𝑥 ( 𝜓 ∨ 𝜑 ) )
4 orcom ⊢ ( ( ∀ 𝑥 𝜑 ∨ 𝜓 ) ↔ ( 𝜓 ∨ ∀ 𝑥 𝜑 ) )
5 1 3 4 3bitr4i ⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∨ 𝜓 ) )