Metamath Proof Explorer


Theorem elmapdd

Description: Deduction associated with elmapd . (Contributed by SN, 29-Jul-2024)

Ref Expression
Hypotheses elmapdd.a φ A V
elmapdd.b φ B W
elmapdd.c φ C : B A
Assertion elmapdd φ C A B

Proof

Step Hyp Ref Expression
1 elmapdd.a φ A V
2 elmapdd.b φ B W
3 elmapdd.c φ C : B A
4 1 2 elmapd φ C A B C : B A
5 3 4 mpbird φ C A B