**Description:** Subclass transitivity inference. (Contributed by NM, 5-May-2000)

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

Hypotheses | sstri.1 | $${\u22a2}{A}\subseteq {B}$$ | |

sstri.2 | $${\u22a2}{B}\subseteq {C}$$ | ||

Assertion | sstri | $${\u22a2}{A}\subseteq {C}$$ |

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

1 | sstri.1 | $${\u22a2}{A}\subseteq {B}$$ | |

2 | sstri.2 | $${\u22a2}{B}\subseteq {C}$$ | |

3 | sstr2 | $${\u22a2}{A}\subseteq {B}\to \left({B}\subseteq {C}\to {A}\subseteq {C}\right)$$ | |

4 | 1 2 3 | mp2 | $${\u22a2}{A}\subseteq {C}$$ |