Metamath Proof Explorer

Theorem unssd

Description: A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypotheses unssd.1 φ A C
unssd.2 φ B C
Assertion unssd φ A B C


Step Hyp Ref Expression
1 unssd.1 φ A C
2 unssd.2 φ B C
3 unss A C B C A B C
4 3 biimpi A C B C A B C
5 1 2 4 syl2anc φ A B C