Metamath Proof Explorer


Theorem ssbrd

Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004)

Ref Expression
Hypothesis ssbrd.1 φ A B
Assertion ssbrd φ C A D C B D

Proof

Step Hyp Ref Expression
1 ssbrd.1 φ A B
2 1 sseld φ C D A C D B
3 df-br C A D C D A
4 df-br C B D C D B
5 2 3 4 3imtr4g φ C A D C B D