Proof 01. ⊢ C ∩ (A ∪ B) = (C ∩ A) ∪ (C ∩ B), intersection_distl. 02. ⊢ (A ∪ B) ∩ C = C ∩ (A ∪ B), intersection_comm. 03. ⊢ (A ∪ B) ∩ C = (C ∩ A) ∪ (C ∩ B), eq_trans 2 1. 04. ⊢ C ∩ A = A ∩ C, intersection_comm. 05. ⊢ (A ∪ B) ∩ C = (A ∩ C) ∪ (C ∩ B), eq_subst 4 3, P X ↔ (A ∪ B) ∩ C = X ∪ (C ∩ B). 06. ⊢ C ∩ B = B ∩ C, intersection_comm. intersection_distr. ⊢ (A ∪ B) ∩ C = (A ∩ C) ∪ (B ∩ C), eq_subst 6 5, P X ↔ (A ∪ B) ∩ C = (A ∩ C) ∪ X.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.