Metamath Proof Explorer


Theorem eelT01

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

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

Proof

Step Hyp Ref Expression
1 eelT01.1 ( ⊤ → 𝜑 )
2 eelT01.2 𝜓
3 eelT01.3 ( 𝜒𝜃 )
4 eelT01.4 ( ( 𝜑𝜓𝜃 ) → 𝜏 )
5 3anass ( ( ⊤ ∧ 𝜓𝜒 ) ↔ ( ⊤ ∧ ( 𝜓𝜒 ) ) )
6 truan ( ( ⊤ ∧ ( 𝜓𝜒 ) ) ↔ ( 𝜓𝜒 ) )
7 simpr ( ( 𝜓𝜒 ) → 𝜒 )
8 2 jctl ( 𝜒 → ( 𝜓𝜒 ) )
9 7 8 impbii ( ( 𝜓𝜒 ) ↔ 𝜒 )
10 5 6 9 3bitri ( ( ⊤ ∧ 𝜓𝜒 ) ↔ 𝜒 )
11 1 4 syl3an1 ( ( ⊤ ∧ 𝜓𝜃 ) → 𝜏 )
12 3 11 syl3an3 ( ( ⊤ ∧ 𝜓𝜒 ) → 𝜏 )
13 10 12 sylbir ( 𝜒𝜏 )