Metamath Proof Explorer


Theorem tpid2g

Description: Closed theorem form of tpid2 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion tpid2g A B A C A D

Proof

Step Hyp Ref Expression
1 eqid A = A
2 1 3mix2i A = C A = A A = D
3 eltpg A B A C A D A = C A = A A = D
4 2 3 mpbiri A B A C A D