# Metamath Proof Explorer

## Theorem in3an

Description: The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a is the non-virtual deduction form of in3an . (Contributed by Alan Sare, 25-Jun-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis in3an.1 ${⊢}\left({\phi }{,}{\psi }{,}\left({\chi }\wedge {\theta }\right){\to }{\tau }\right)$
Assertion in3an ${⊢}\left({\phi }{,}{\psi }{,}{\chi }{\to }\left({\theta }\to {\tau }\right)\right)$

### Proof

Step Hyp Ref Expression
1 in3an.1 ${⊢}\left({\phi }{,}{\psi }{,}\left({\chi }\wedge {\theta }\right){\to }{\tau }\right)$
2 1 dfvd3i ${⊢}{\phi }\to \left({\psi }\to \left(\left({\chi }\wedge {\theta }\right)\to {\tau }\right)\right)$
3 2 exp4a ${⊢}{\phi }\to \left({\psi }\to \left({\chi }\to \left({\theta }\to {\tau }\right)\right)\right)$
4 3 dfvd3ir ${⊢}\left({\phi }{,}{\psi }{,}{\chi }{\to }\left({\theta }\to {\tau }\right)\right)$