Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eelTT Structured version   Visualization version   GIF version

Theorem eelTT 38466
 Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
eelTT.1 (⊤ → 𝜑)
eelTT.2 (⊤ → 𝜓)
eelTT.3 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
eelTT 𝜒

Proof of Theorem eelTT
StepHypRef Expression
1 eelTT.2 . . 3 (⊤ → 𝜓)
2 truan 1498 . . . 4 ((⊤ ∧ 𝜓) ↔ 𝜓)
3 eelTT.1 . . . . 5 (⊤ → 𝜑)
4 eelTT.3 . . . . 5 ((𝜑𝜓) → 𝜒)
53, 4sylan 488 . . . 4 ((⊤ ∧ 𝜓) → 𝜒)
62, 5sylbir 225 . . 3 (𝜓𝜒)
71, 6syl 17 . 2 (⊤ → 𝜒)
87trud 1490 1 𝜒
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384  ⊤wtru 1481 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator