Description: A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan BenNaim, 3Jun2011)
Ref  Expression  

Hypotheses  unssd.1   ( ph > A C_ C ) 

unssd.2   ( ph > B C_ C ) 

Assertion  unssd   ( ph > ( A u. B ) C_ C ) 
Step  Hyp  Ref  Expression 

1  unssd.1   ( ph > A C_ C ) 

2  unssd.2   ( ph > B C_ C ) 

3  unss   ( ( A C_ C /\ B C_ C ) <> ( A u. B ) C_ C ) 

4  3  biimpi   ( ( A C_ C /\ B C_ C ) > ( A u. B ) C_ C ) 
5  1 2 4  syl2anc   ( ph > ( A u. B ) C_ C ) 