Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  resolution Structured version   Visualization version   GIF version

Theorem resolution 47332
Description: Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.)
Assertion
Ref Expression
resolution (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → (𝜓𝜒))

Proof of Theorem resolution
StepHypRef Expression
1 simpr 486 . 2 ((𝜑𝜓) → 𝜓)
2 simpr 486 . 2 ((¬ 𝜑𝜒) → 𝜒)
31, 2orim12i 908 1 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 846
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 206  df-an 398  df-or 847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator