Theorem ssbrd 4444

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 3431	. 2 |- ( ph -> ( <. C , D >. e. A -> <. C , D >. e. B ) )
3		df-br 4403	. 2 |- ( C A D <-> <. C , D >. e. A )
4		df-br 4403	. 2 |- ( C B D <-> <. C , D >. e. B )
5	2, 3, 4	3imtr4g 274	1 |- ( ph -> ( C A D -> C B D ) )

Syntax hints:   -> wi 4   e. wcel 1887   C_ wss 3404   <.cop 3974   class class class wbr 4402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418  df-br 4403

This theorem is referenced by:  ssbri  4445  sess1  4802  brrelex12  4872  coss1  4990  coss2  4991  eqbrrdva  5004  ersym  7375  ertr  7378  fpwwe2lem6  9060  fpwwe2lem7  9061  fpwwe2lem9  9063  fpwwe2lem12  9066  fpwwe2lem13  9067  fpwwe2  9068  coss12d  13036  fthres2  15837  invfuc  15879  pospo  16219  dirref  16481  efgcpbl  17406  frgpuplem  17422  subrguss  18023  znleval  19125  ustref  21233  ustuqtop4  21259  isucn2  21294  brelg  28217  metider  28697  mclsppslem  30221  fundmpss  30407  iunrelexpuztr  36311  frege96d  36341  frege91d  36343  frege98d  36345  frege124d  36353  ssrelrn  39012