# Metamath Proof Explorer

## Theorem e223

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 e223.1 ${⊢}\left({\phi }{,}{\psi }{\to }{\chi }\right)$
2 e223.2 ${⊢}\left({\phi }{,}{\psi }{\to }{\theta }\right)$
3 e223.3 ${⊢}\left({\phi }{,}{\psi }{,}{\tau }{\to }{\eta }\right)$
4 e223.4 ${⊢}{\chi }\to \left({\theta }\to \left({\eta }\to {\zeta }\right)\right)$
5 1 in2 ${⊢}\left({\phi }{\to }\left({\psi }\to {\chi }\right)\right)$
6 5 in1 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
7 2 in2 ${⊢}\left({\phi }{\to }\left({\psi }\to {\theta }\right)\right)$
8 7 in1 ${⊢}{\phi }\to \left({\psi }\to {\theta }\right)$
9 3 in3 ${⊢}\left({\phi }{,}{\psi }{\to }\left({\tau }\to {\eta }\right)\right)$
10 9 in2 ${⊢}\left({\phi }{\to }\left({\psi }\to \left({\tau }\to {\eta }\right)\right)\right)$
11 10 in1 ${⊢}{\phi }\to \left({\psi }\to \left({\tau }\to {\eta }\right)\right)$
12 6 8 11 4 ee223 ${⊢}{\phi }\to \left({\psi }\to \left({\tau }\to {\zeta }\right)\right)$
13 12 dfvd3ir ${⊢}\left({\phi }{,}{\psi }{,}{\tau }{\to }{\zeta }\right)$