Metamath Proof Explorer


Theorem fvtp2g

Description: The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)

Ref Expression
Assertion fvtp2g BVEWABBCADBECFB=E

Proof

Step Hyp Ref Expression
1 tprot ADBECF=BECFAD
2 1 fveq1i ADBECFB=BECFADB
3 necom ABBA
4 fvtp1g BVEWBCBABECFADB=E
5 4 expcom BCBABVEWBECFADB=E
6 5 ancoms BABCBVEWBECFADB=E
7 3 6 sylanb ABBCBVEWBECFADB=E
8 7 impcom BVEWABBCBECFADB=E
9 2 8 eqtrid BVEWABBCADBECFB=E