Theorem eel000cT

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

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

Proof

Step	Hyp	Ref	Expression
1		eel000cT.1	$$⊢\phi$$
2		eel000cT.2	$$⊢\psi$$
3		eel000cT.3	$$⊢\chi$$
4		eel000cT.4	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\to \theta$$
5	1 4	mp3an1	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
6	2 5	mpan	$$⊢\chi \to \theta$$
7	3 6	ax-mp	$$⊢\theta$$
8	7	a1i	$$⊢\top \to \theta$$