**Description:** Closure law for multiplication. (Contributed by NM, 23-Nov-1994)

Ref | Expression | ||
---|---|---|---|

Hypotheses | axi.1 | $${\u22a2}{A}\in \u2102$$ | |

axi.2 | $${\u22a2}{B}\in \u2102$$ | ||

Assertion | mulcli | $${\u22a2}{A}{B}\in \u2102$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | axi.1 | $${\u22a2}{A}\in \u2102$$ | |

2 | axi.2 | $${\u22a2}{B}\in \u2102$$ | |

3 | mulcl | $${\u22a2}\left({A}\in \u2102\wedge {B}\in \u2102\right)\to {A}{B}\in \u2102$$ | |

4 | 1 2 3 | mp2an | $${\u22a2}{A}{B}\in \u2102$$ |