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	⊢ (    𝜑    ▶    𝜓    )
	e111.2	⊢ (    𝜑    ▶    𝜒    )
	e111.3	⊢ (    𝜑    ▶    𝜃    )
	e111.4	⊢ ( 𝜓 → ( 𝜒 → ( 𝜃 → 𝜏 ) ) )
Assertion	e111	⊢ (    𝜑    ▶    𝜏    )

Proof

Step	Hyp	Ref	Expression
1		e111.1	⊢ (    𝜑    ▶    𝜓    )
2		e111.2	⊢ (    𝜑    ▶    𝜒    )
3		e111.3	⊢ (    𝜑    ▶    𝜃    )
4		e111.4	⊢ ( 𝜓 → ( 𝜒 → ( 𝜃 → 𝜏 ) ) )
5	3	in1	⊢ ( 𝜑 → 𝜃 )
6	1	in1	⊢ ( 𝜑 → 𝜓 )
7	2	in1	⊢ ( 𝜑 → 𝜒 )
8	6 7 4	syl2im	⊢ ( 𝜑 → ( 𝜑 → ( 𝜃 → 𝜏 ) ) )
9	8	pm2.43i	⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) )
10	5 9	syl5com	⊢ ( 𝜑 → ( 𝜑 → 𝜏 ) )
11	10	pm2.43i	⊢ ( 𝜑 → 𝜏 )
12	11	dfvd1ir	⊢ (    𝜑    ▶    𝜏    )