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)$$