# Metamath Proof Explorer

## Theorem e111

Description: A virtual deduction elimination rule (see syl3c ). (Contributed by Alan Sare, 14-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 e111.1 ${⊢}\left({\phi }{\to }{\psi }\right)$
2 e111.2 ${⊢}\left({\phi }{\to }{\chi }\right)$
3 e111.3 ${⊢}\left({\phi }{\to }{\theta }\right)$
4 e111.4 ${⊢}{\psi }\to \left({\chi }\to \left({\theta }\to {\tau }\right)\right)$
5 3 in1 ${⊢}{\phi }\to {\theta }$
6 1 in1 ${⊢}{\phi }\to {\psi }$
7 2 in1 ${⊢}{\phi }\to {\chi }$
8 6 7 4 syl2im ${⊢}{\phi }\to \left({\phi }\to \left({\theta }\to {\tau }\right)\right)$
9 8 pm2.43i ${⊢}{\phi }\to \left({\theta }\to {\tau }\right)$
10 5 9 syl5com ${⊢}{\phi }\to \left({\phi }\to {\tau }\right)$
11 10 pm2.43i ${⊢}{\phi }\to {\tau }$
12 11 dfvd1ir ${⊢}\left({\phi }{\to }{\tau }\right)$