**Description:** Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014)

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

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

sstrid.2 | $${\u22a2}{\phi}\to {B}\subseteq {C}$$ | ||

Assertion | sstrid | $${\u22a2}{\phi}\to {A}\subseteq {C}$$ |

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

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

2 | sstrid.2 | $${\u22a2}{\phi}\to {B}\subseteq {C}$$ | |

3 | 1 | a1i | $${\u22a2}{\phi}\to {A}\subseteq {B}$$ |

4 | 3 2 | sstrd | $${\u22a2}{\phi}\to {A}\subseteq {C}$$ |