This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tpid3g

Description: Closed theorem form of tpid3 . (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by JJ, 30-Apr-2021)

Ref Expression
Assertion tpid3g ⊢ A ∈ B → A ∈ C D A

Proof

Step Hyp Ref Expression
1 eqid ⊢ A = A
2 1 3mix3i ⊢ A = C ∨ A = D ∨ A = A
3 eltpg ⊢ A ∈ B → A ∈ C D A ↔ A = C ∨ A = D ∨ A = A
4 2 3 mpbiri ⊢ A ∈ B → A ∈ C D A