Metamath Proof Explorer


Theorem mpoeq123dv

Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011)

Ref Expression
Hypotheses mpoeq123dv.1 φA=D
mpoeq123dv.2 φB=E
mpoeq123dv.3 φC=F
Assertion mpoeq123dv φxA,yBC=xD,yEF

Proof

Step Hyp Ref Expression
1 mpoeq123dv.1 φA=D
2 mpoeq123dv.2 φB=E
3 mpoeq123dv.3 φC=F
4 2 adantr φxAB=E
5 3 adantr φxAyBC=F
6 1 4 5 mpoeq123dva φxA,yBC=xD,yEF