Theorem eelT01

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

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

Proof

Step	Hyp	Ref	Expression
1		eelT01.1	$$⊢\top \to \phi$$
2		eelT01.2	$$⊢\psi$$
3		eelT01.3	$$⊢\chi \to \theta$$
4		eelT01.4	$$⊢\left(\phi \wedge \psi \wedge \theta \right)\to \tau$$
5		3anass	$$⊢\left(\top \wedge \psi \wedge \chi \right)\leftrightarrow \left(\top \wedge \left(\psi \wedge \chi \right)\right)$$
6		truan	$$⊢\left(\top \wedge \left(\psi \wedge \chi \right)\right)\leftrightarrow \left(\psi \wedge \chi \right)$$
7		simpr	$$⊢\left(\psi \wedge \chi \right)\to \chi$$
8	2	jctl	$$⊢\chi \to \left(\psi \wedge \chi \right)$$
9	7 8	impbii	$$⊢\left(\psi \wedge \chi \right)\leftrightarrow \chi$$
10	5 6 9	3bitri	$$⊢\left(\top \wedge \psi \wedge \chi \right)\leftrightarrow \chi$$
11	1 4	syl3an1	$$⊢\left(\top \wedge \psi \wedge \theta \right)\to \tau$$
12	3 11	syl3an3	$$⊢\left(\top \wedge \psi \wedge \chi \right)\to \tau$$
13	10 12	sylbir	$$⊢\chi \to \tau$$