Metamath Proof Explorer

Theorem fssd

Description: Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fssd.f φ F : A B
fssd.b φ B C
Assertion fssd φ F : A C


Step Hyp Ref Expression
1 fssd.f φ F : A B
2 fssd.b φ B C
3 fss F : A B B C F : A C
4 1 2 3 syl2anc φ F : A C