Theorem ssbrd 4474

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

Hypothesis

Ref	Expression
ssbrd.1	|- ( ph -> A C_ B )

Assertion

Ref	Expression
ssbrd	|- ( ph -> ( C A D -> C B D ) )

Proof of Theorem ssbrd

Step	Hyp	Ref	Expression
1		ssbrd.1	. . 3 |- ( ph -> A C_ B )
2	1	sseld 3485	. 2 |- ( ph -> ( <. C , D >. e. A -> <. C , D >. e. B ) )
3		df-br 4434	. 2 |- ( C A D <-> <. C , D >. e. A )
4		df-br 4434	. 2 |- ( C B D <-> <. C , D >. e. B )
5	2, 3, 4	3imtr4g 270	1 |- ( ph -> ( C A D -> C B D ) )

Syntax hints:   -> wi 4   e. wcel 1802   C_ wss 3458   <.cop 4016   class class class wbr 4433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472  df-br 4434

This theorem is referenced by:  ssbri  4475  sess1  4833  brrelex12  5023  coss1  5144  coss2  5145  eqbrrdva  5158  ersym  7321  ertr  7324  fpwwe2lem6  9011  fpwwe2lem7  9012  fpwwe2lem9  9014  fpwwe2lem12  9017  fpwwe2lem13  9018  fpwwe2  9019  fthres2  15170  invfuc  15212  pospo  15472  dirref  15734  efgcpbl  16643  frgpuplem  16659  subrguss  17312  znleval  18460  ustref  20587  ustuqtop4  20613  isucn2  20648  brelg  27327  metider  27739  mclsppslem  28809  fundmpss  29164  coss12d  37424