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	⊢ 𝜑
	eel0TT.2	⊢ ( ⊤ → 𝜓 )
	eel0TT.3	⊢ ( ⊤ → 𝜒 )
	eel0TT.4	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion	eel0TT	⊢ 𝜃

Proof

Step	Hyp	Ref	Expression
1		eel0TT.1	⊢ 𝜑
2		eel0TT.2	⊢ ( ⊤ → 𝜓 )
3		eel0TT.3	⊢ ( ⊤ → 𝜒 )
4		eel0TT.4	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5		truan	⊢ ( ( ⊤ ∧ 𝜒 ) ↔ 𝜒 )
6	1 4	mp3an1	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
7	2 6	sylan	⊢ ( ( ⊤ ∧ 𝜒 ) → 𝜃 )
8	5 7	sylbir	⊢ ( 𝜒 → 𝜃 )
9	3 8	syl	⊢ ( ⊤ → 𝜃 )
10	9	mptru	⊢ 𝜃