Theorem resolution 47933

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 483	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2		simpr 483	. 2 ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜒)
3	1, 2	orim12i 905	1 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → (𝜓 ∨ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∨ 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 206  df-an 395  df-or 844

This theorem is referenced by: (None)