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

Ref | Expression | ||
---|---|---|---|

Assertion | tpid3g | $${\u22a2}{A}\in {B}\to {A}\in \left\{{C},{D},{A}\right\}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eqid | $${\u22a2}{A}={A}$$ | |

2 | 1 | 3mix3i | $${\u22a2}\left({A}={C}\vee {A}={D}\vee {A}={A}\right)$$ |

3 | eltpg | $${\u22a2}{A}\in {B}\to \left({A}\in \left\{{C},{D},{A}\right\}\leftrightarrow \left({A}={C}\vee {A}={D}\vee {A}={A}\right)\right)$$ | |

4 | 2 3 | mpbiri | $${\u22a2}{A}\in {B}\to {A}\in \left\{{C},{D},{A}\right\}$$ |