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	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → ( 𝜓 ∨ 𝜒 ) )