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

Metamath Proof Explorer

Theorem eelT11

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

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

Proof

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