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

Metamath Proof Explorer

Theorem eelT00

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

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

Proof

Step Hyp Ref Expression
1 eelT00.1 ⊢ ( ⊤ → 𝜑 )
2 eelT00.2 ⊢ 𝜓
3 eelT00.3 ⊢ 𝜒
4 eelT00.4 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5 3anass ⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) )
6 truan ⊢ ( ( ⊤ ∧ ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜓 ∧ 𝜒 ) )
7 5 6 bitri ⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) )
8 1 4 syl3an1 ⊢ ( ( ⊤ ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
9 7 8 sylbir ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
10 2 9 mpan ⊢ ( 𝜒 → 𝜃 )
11 3 10 ax-mp ⊢ 𝜃