Theorem resolution 50303

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

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

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

This theorem is referenced by: (None)