Theorem eel0TT

Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	eel0TT.1	$$⊢\phi$$
	eel0TT.2	$$⊢\top \to \psi$$
	eel0TT.3	$$⊢\top \to \chi$$
	eel0TT.4	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\to \theta$$
Assertion	eel0TT	$$⊢\theta$$

Proof

Step	Hyp	Ref	Expression
1		eel0TT.1	$$⊢\phi$$
2		eel0TT.2	$$⊢\top \to \psi$$
3		eel0TT.3	$$⊢\top \to \chi$$
4		eel0TT.4	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\to \theta$$
5		truan	$$⊢\left(\top \wedge \chi \right)\leftrightarrow \chi$$
6	1 4	mp3an1	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
7	2 6	sylan	$$⊢\left(\top \wedge \chi \right)\to \theta$$
8	5 7	sylbir	$$⊢\chi \to \theta$$
9	3 8	syl	$$⊢\top \to \theta$$
10	9	mptru	$$⊢\theta$$