# Metamath Proof Explorer

## Theorem eelT11

Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses eelT11.1 ${⊢}\top \to {\phi }$
eelT11.2 ${⊢}{\psi }\to {\chi }$
eelT11.3 ${⊢}{\psi }\to {\theta }$
eelT11.4 ${⊢}\left({\phi }\wedge {\chi }\wedge {\theta }\right)\to {\tau }$
Assertion eelT11 ${⊢}{\psi }\to {\tau }$

### Proof

Step Hyp Ref Expression
1 eelT11.1 ${⊢}\top \to {\phi }$
2 eelT11.2 ${⊢}{\psi }\to {\chi }$
3 eelT11.3 ${⊢}{\psi }\to {\theta }$
4 eelT11.4 ${⊢}\left({\phi }\wedge {\chi }\wedge {\theta }\right)\to {\tau }$
5 3anass ${⊢}\left(\top \wedge {\psi }\wedge {\psi }\right)↔\left(\top \wedge \left({\psi }\wedge {\psi }\right)\right)$
6 truan ${⊢}\left(\top \wedge \left({\psi }\wedge {\psi }\right)\right)↔\left({\psi }\wedge {\psi }\right)$
7 anidm ${⊢}\left({\psi }\wedge {\psi }\right)↔{\psi }$
8 5 6 7 3bitri ${⊢}\left(\top \wedge {\psi }\wedge {\psi }\right)↔{\psi }$
9 1 4 syl3an1 ${⊢}\left(\top \wedge {\chi }\wedge {\theta }\right)\to {\tau }$
10 2 9 syl3an2 ${⊢}\left(\top \wedge {\psi }\wedge {\theta }\right)\to {\tau }$
11 3 10 syl3an3 ${⊢}\left(\top \wedge {\psi }\wedge {\psi }\right)\to {\tau }$
12 8 11 sylbir ${⊢}{\psi }\to {\tau }$