Theorem eelT12

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

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

Proof

Step	Hyp	Ref	Expression
1		eelT12.1	⊢ ( ⊤ → 𝜑 )
2		eelT12.2	⊢ ( 𝜓 → 𝜒 )
3		eelT12.3	⊢ ( 𝜃 → 𝜏 )
4		eelT12.4	⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜏 ) → 𝜂 )
5		3anass	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜃 ) ↔ ( ⊤ ∧ ( 𝜓 ∧ 𝜃 ) ) )
6		truan	⊢ ( ( ⊤ ∧ ( 𝜓 ∧ 𝜃 ) ) ↔ ( 𝜓 ∧ 𝜃 ) )
7	5 6	bitri	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜃 ) ↔ ( 𝜓 ∧ 𝜃 ) )
8	1 4	syl3an1	⊢ ( ( ⊤ ∧ 𝜒 ∧ 𝜏 ) → 𝜂 )
9	2 8	syl3an2	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜏 ) → 𝜂 )
10	3 9	syl3an3	⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜃 ) → 𝜂 )
11	7 10	sylbir	⊢ ( ( 𝜓 ∧ 𝜃 ) → 𝜂 )