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

Theorem eel12131 37959
 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 . . . . . 6 ((𝜑𝜏) → 𝜂)
2 eel12131.2 . . . . . . . . . 10 ((𝜑𝜒) → 𝜃)
3 eel12131.1 . . . . . . . . . . 11 (𝜑𝜓)
4 eel12131.4 . . . . . . . . . . . 12 ((𝜓𝜃𝜂) → 𝜁)
543exp 1256 . . . . . . . . . . 11 (𝜓 → (𝜃 → (𝜂𝜁)))
63, 5syl 17 . . . . . . . . . 10 (𝜑 → (𝜃 → (𝜂𝜁)))
72, 6syl5com 31 . . . . . . . . 9 ((𝜑𝜒) → (𝜑 → (𝜂𝜁)))
87ex 449 . . . . . . . 8 (𝜑 → (𝜒 → (𝜑 → (𝜂𝜁))))
98pm2.43b 53 . . . . . . 7 (𝜒 → (𝜑 → (𝜂𝜁)))
109com13 86 . . . . . 6 (𝜂 → (𝜑 → (𝜒𝜁)))
111, 10syl 17 . . . . 5 ((𝜑𝜏) → (𝜑 → (𝜒𝜁)))
1211ex 449 . . . 4 (𝜑 → (𝜏 → (𝜑 → (𝜒𝜁))))
1312pm2.43b 53 . . 3 (𝜏 → (𝜑 → (𝜒𝜁)))
1413com3l 87 . 2 (𝜑 → (𝜒 → (𝜏𝜁)))
15143imp 1249 1 ((𝜑𝜒𝜏) → 𝜁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  isosctrlem1ALT  38192
 Copyright terms: Public domain W3C validator