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 φAB
Assertion ssbrd φCADCBD

Proof

Step Hyp Ref Expression
1 ssbrd.1 φAB
2 1 sseld φCDACDB
3 df-br CADCDA
4 df-br CBDCDB
5 2 3 4 3imtr4g φCADCBD