Theorem eelT00

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

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

Proof

Step	Hyp	Ref	Expression
1		eelT00.1	⊢ ( ⊤ → 𝜑 )
2		eelT00.2	⊢ 𝜓
3		eelT00.3	⊢ 𝜒
4		eelT00.4	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5		3anass	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) )
6		truan	⊢ ( ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜓 ∧ 𝜒 ) )
7	5 6	bitri	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) )
8	1 4	syl3an1	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
9	7 8	sylbir	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
10	2 9	mpan	⊢ ( 𝜒 → 𝜃 )
11	3 10	ax-mp	⊢ 𝜃