Metamath Proof Explorer


Theorem elmapd

Description: Deduction form of elmapg . (Contributed by BJ, 11-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 elmapd.a φ A V
2 elmapd.b φ B W
3 elmapg A V B W C A B C : B A
4 1 2 3 syl2anc φ C A B C : B A