Theorem elin3

Description: Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypothesis	elin3.x	⊢ 𝑋 = ( ( 𝐵 ∩ 𝐶 ) ∩ 𝐷 )
Assertion	elin3	⊢ ( 𝐴 ∈ 𝑋 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		elin3.x	⊢ 𝑋 = ( ( 𝐵 ∩ 𝐶 ) ∩ 𝐷 )
2		elin	⊢ ( 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )
3	2	anbi1i	⊢ ( ( 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝐴 ∈ 𝐷 ) ↔ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ∧ 𝐴 ∈ 𝐷 ) )
4	1	elin2	⊢ ( 𝐴 ∈ 𝑋 ↔ ( 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝐴 ∈ 𝐷 ) )
5		df-3an	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷 ) ↔ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ∧ 𝐴 ∈ 𝐷 ) )
6	3 4 5	3bitr4i	⊢ ( 𝐴 ∈ 𝑋 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷 ) )