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

Theorem resolution 28518
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  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ch ) )  -> 
( ps  \/  ch ) )

Proof of Theorem resolution
StepHypRef Expression
1 simpr 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
2 simpr 447 . 2  |-  ( ( -.  ph  /\  ch )  ->  ch )
31, 2orim12i 502 1  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ch ) )  -> 
( ps  \/  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator