Theorem resolution 44894

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

Step	Hyp	Ref	Expression
1		simpr 487	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2		simpr 487	. 2 ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜒)
3	1, 2	orim12i 905	1 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → (𝜓 ∨ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by: (None)