Theorem eel0T1

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

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

Proof

Step	Hyp	Ref	Expression
1		eel0T1.1	⊢ 𝜑
2		eel0T1.2	⊢ ( ⊤ → 𝜓 )
3		eel0T1.3	⊢ ( 𝜒 → 𝜃 )
4		eel0T1.4	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜃 ) → 𝜏 )
5		3anass	⊢ ( ( 𝜑 ∧ ⊤ ∧ 𝜒 ) ↔ ( 𝜑 ∧ ( ⊤ ∧ 𝜒 ) ) )
6		simpr	⊢ ( ( 𝜑 ∧ ( ⊤ ∧ 𝜒 ) ) → ( ⊤ ∧ 𝜒 ) )
7	1	jctl	⊢ ( ( ⊤ ∧ 𝜒 ) → ( 𝜑 ∧ ( ⊤ ∧ 𝜒 ) ) )
8	6 7	impbii	⊢ ( ( 𝜑 ∧ ( ⊤ ∧ 𝜒 ) ) ↔ ( ⊤ ∧ 𝜒 ) )
9		truan	⊢ ( ( ⊤ ∧ 𝜒 ) ↔ 𝜒 )
10	5 8 9	3bitri	⊢ ( ( 𝜑 ∧ ⊤ ∧ 𝜒 ) ↔ 𝜒 )
11	2 4	syl3an2	⊢ ( ( 𝜑 ∧ ⊤ ∧ 𝜃 ) → 𝜏 )
12	3 11	syl3an3	⊢ ( ( 𝜑 ∧ ⊤ ∧ 𝜒 ) → 𝜏 )
13	10 12	sylbir	⊢ ( 𝜒 → 𝜏 )