Theorem pm10.55

Description: Theorem *10.55 in WhiteheadRussell p. 156. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	pm10.55	⊢ ( ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) ↔ ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		exsimpl	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 𝜑 )
2	1	anim1i	⊢ ( ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
3		exintr	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
4	3	imdistanri	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
5	2 4	impbii	⊢ ( ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) ↔ ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )