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

Theorem eel12131 39440
 Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
Hypotheses
Ref Expression
eel12131.1 (𝜑𝜓)
eel12131.2 ((𝜑𝜒) → 𝜃)
eel12131.3 ((𝜑𝜏) → 𝜂)
eel12131.4 ((𝜓𝜃𝜂) → 𝜁)
Assertion
Ref Expression
eel12131 ((𝜑𝜒𝜏) → 𝜁)

Proof of Theorem eel12131
StepHypRef Expression
1 eel12131.3 . . . . 5 ((𝜑𝜏) → 𝜂)
2 eel12131.1 . . . . . . . . 9 (𝜑𝜓)
3 eel12131.2 . . . . . . . . 9 ((𝜑𝜒) → 𝜃)
4 eel12131.4 . . . . . . . . . 10 ((𝜓𝜃𝜂) → 𝜁)
543exp 1113 . . . . . . . . 9 (𝜓 → (𝜃 → (𝜂𝜁)))
62, 3, 5syl2imc 41 . . . . . . . 8 ((𝜑𝜒) → (𝜑 → (𝜂𝜁)))
76ex 449 . . . . . . 7 (𝜑 → (𝜒 → (𝜑 → (𝜂𝜁))))
87pm2.43b 55 . . . . . 6 (𝜒 → (𝜑 → (𝜂𝜁)))
98com13 88 . . . . 5 (𝜂 → (𝜑 → (𝜒𝜁)))
101, 9syl 17 . . . 4 ((𝜑𝜏) → (𝜑 → (𝜒𝜁)))
1110ex 449 . . 3 (𝜑 → (𝜏 → (𝜑 → (𝜒𝜁))))
1211pm2.43b 55 . 2 (𝜏 → (𝜑 → (𝜒𝜁)))
13123imp231 1105 1 ((𝜑𝜒𝜏) → 𝜁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072 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 385  df-3an 1074 This theorem is referenced by:  isosctrlem1ALT  39669
 Copyright terms: Public domain W3C validator