Metamath Proof Explorer

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 ⊢ ψ ∧ θ → η