| ⊢ | (f g) ∧ (f g1) ≡ f (g ∧ g1) | YieldsAndYieldsEqvYieldsAnd |
Proof:
1 | ⊢ f ; (¬g ∨¬g1) ≡ (f ; ¬g) ∨ (f ; ¬g1) | |
2 | ⊢ (f ; ¬g) ∨ (f ; ¬g1) ≡ f ; (¬g ∨¬g1) | |
3 | ⊢ ¬g ∨¬g1 ≡¬(g ∧ g1) | |
4 | ⊢ f ; (¬g ∨¬g1) ≡ f ; ¬(g ∧ g1) | |
5 | ⊢ (f ; ¬g) ∨ (f ; ¬g1) ≡ f ; ¬(g ∧ g1) | |
6 | ⊢ ¬(f ; ¬g) ∧¬(f ; ¬g1) ≡¬(f ; ¬(g ∧ g1)) | |
7 | ⊢ (f g) ∧ (f g1) ≡ f (g ∧ g1) | 6, def. of |
qed