This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝜃