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

Metamath Proof Explorer

Theorem pm11.53v

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

		Ref	Expression
	Assertion	pm11.53v	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )

Step	Hyp	Ref	Expression
1		19.21v	⊢ ( ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑦 𝜓 ) )
2	1	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) )
3		19.23v	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )
4	2 3	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )