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

Metamath Proof Explorer

Theorem eelTTT

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

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

Proof

Step Hyp Ref Expression
1 eelTTT.1 ⊢ ( ⊤ → 𝜑 )
2 eelTTT.2 ⊢ ( ⊤ → 𝜓 )
3 eelTTT.3 ⊢ ( ⊤ → 𝜒 )
4 eelTTT.4 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5 truan ⊢ ( ( ⊤ ∧ 𝜒 ) ↔ 𝜒 )
6 3anass ⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) )
7 truan ⊢ ( ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜓 ∧ 𝜒 ) )
8 6 7 bitri ⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) )
9 1 4 syl3an1 ⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
10 8 9 sylbir ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
11 2 10 sylan ⊢ ( ( ⊤ ∧ 𝜒 ) → 𝜃 )
12 5 11 sylbir ⊢ ( 𝜒 → 𝜃 )
13 3 12 syl ⊢ ( ⊤ → 𝜃 )
14 13 mptru ⊢ 𝜃