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

Metamath Proof Explorer

Theorem eel000cT

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

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

Proof

Step Hyp Ref Expression
1 eel000cT.1 ⊢ 𝜑
2 eel000cT.2 ⊢ 𝜓
3 eel000cT.3 ⊢ 𝜒
4 eel000cT.4 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5 1 4 mp3an1 ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
6 2 5 mpan ⊢ ( 𝜒 → 𝜃 )
7 3 6 ax-mp ⊢ 𝜃
8 7 a1i ⊢ ( ⊤ → 𝜃 )