Theorem eelTTT

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

	Ref	Expression
Hypotheses	eelTTT.1	⊢ ( ⊤ → 𝜑 )
	eelTTT.2	⊢ ( ⊤ → 𝜓 )
	eelTTT.3	⊢ ( ⊤ → 𝜒 )
	eelTTT.4	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion	eelTTT	⊢ 𝜃

Proof

Step	Hyp	Ref	Expression
1		eelTTT.1	⊢ ( ⊤ → 𝜑 )
2		eelTTT.2	⊢ ( ⊤ → 𝜓 )
3		eelTTT.3	⊢ ( ⊤ → 𝜒 )
4		eelTTT.4	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5		truan	⊢ ( ( ⊤ ∧ 𝜒 ) ↔ 𝜒 )
6		3anass	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) )
7		truan	⊢ ( ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜓 ∧ 𝜒 ) )
8	6 7	bitri	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) )
9	1 4	syl3an1	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
10	8 9	sylbir	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
11	2 10	sylan	⊢ ( ( ⊤ ∧ 𝜒 ) → 𝜃 )
12	5 11	sylbir	⊢ ( 𝜒 → 𝜃 )
13	3 12	syl	⊢ ( ⊤ → 𝜃 )
14	13	mptru	⊢ 𝜃