| ⊢ | (f g) ∧ (f1 g1) ⊃ (f ∧ f1) (g ∧ g1) | YieldsAndYieldsImpAndYieldsAnd |
Proof:
1 | ⊢ f g ⊃ (f ∧ f1) g | |
2 | ⊢ f1 g1 ⊃ (f ∧ f1) g1 | |
3 | ⊢ (f ∧ f1) g ∧ (f ∧ f1) g1 ≡ (f ∧ f1) (g ∧ g1) | |
4 | ⊢ (f g) ∧ (f1 g1) ⊃ (f ∧ f1) (g ∧ g1) |
qed