Theorem pm11.6

Description: Theorem *11.6 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 25-May-2011)

	Ref	Expression
Assertion	pm11.6	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ∃ 𝑦 ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		excom	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
2		an32	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )
3	2	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )
4	1 3	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )
5		19.41v	⊢ ( ∃ 𝑦 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
6	5	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
7		19.41v	⊢ ( ∃ 𝑥 ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) ↔ ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )
8	7	exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) ↔ ∃ 𝑦 ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )
9	4 6 8	3bitr3i	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ∃ 𝑦 ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) )