Metamath Proof Explorer


Theorem resolution

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)

Ref Expression
Assertion resolution ( ( ( 𝜑𝜓 ) ∨ ( ¬ 𝜑𝜒 ) ) → ( 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝜑𝜓 ) → 𝜓 )
2 simpr ( ( ¬ 𝜑𝜒 ) → 𝜒 )
3 1 2 orim12i ( ( ( 𝜑𝜓 ) ∨ ( ¬ 𝜑𝜒 ) ) → ( 𝜓𝜒 ) )