Theorem resolution 47846

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 846

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 398  df-or 847

This theorem is referenced by: (None)