Theorem ssbrd 4434

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 3456	. 2 |- ( ph -> ( <. C , D >. e. A -> <. C , D >. e. B ) )
3		df-br 4394	. 2 |- ( C A D <-> <. C , D >. e. A )
4		df-br 4394	. 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 1758   C_ wss 3429   <.cop 3984   class class class wbr 4393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3436  df-ss 3443  df-br 4394

This theorem is referenced by:  ssbri  4435  sess1  4789  brrelex12  4977  coss1  5096  coss2  5097  eqbrrdva  5110  ersym  7216  ertr  7219  fpwwe2lem6  8906  fpwwe2lem7  8907  fpwwe2lem9  8909  fpwwe2lem12  8912  fpwwe2lem13  8913  fpwwe2  8914  fthres2  14953  invfuc  14995  pospo  15254  dirref  15516  efgcpbl  16366  frgpuplem  16382  subrguss  16995  znleval  18105  ustref  19918  ustuqtop4  19944  isucn2  19979  brelg  26085  metider  26459  fundmpss  27714