Description: Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007) (Revised by Mario Carneiro, 8-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ssbri.1 | |- A C_ B |
|
| Assertion | ssbri | |- ( C A D -> C B D ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssbri.1 | |- A C_ B |
|
| 2 | ssbr | |- ( A C_ B -> ( C A D -> C B D ) ) |
|
| 3 | 1 2 | ax-mp | |- ( C A D -> C B D ) |