Formal Proof of WFF using Rules of Inference

Question

I am currently hung up on a practice problem that requires a formal proof of a WFF using ONLY rules of inference. I've been attempting this for hours, but it seems like there is something i'm missing. In this case, I know I need to get a C or ¬C to use Modus Ponens then Addition, but its not working for me.

WFF: (C→A) ∧ (¬C→B) → A∨B

[EDIT] Latest attempt:

1. (C→A) | Premise for Conditional Proof

2. (¬C→B) | Premise for Conditional Proof

3. ¬C | Premise for Indirect Proof

4. B | 2, 3 Modus Ponens

5. A∨B | 4, Addition

6. ¬C∧B | 3, 4 Conjunction

Answer 1

You are on the right trail. You may either:

(1) Accept the Law of Excluded Middle as an axiom, and eliminate that disjunction.

• $(C\to A)~\land ~(\neg C\to B)$ by premise.
• $C\vee\neg C$ by LEM
  • $C$ by assumption
  • yadayadayadah.
  • $A\vee B$ by reasons
• $C\to(A\vee B)$ by conditional introduction
  • $\neg C$ by assumption
  • $\neg C\to B$ by conjunction elimination (simplification)
  • $B$ by conditional elimination (modus ponens)
  • $A\vee B$ by disjunction introduction
• $\neg C\to(A\vee B)$ by conditional introduction (deduction)
• $A\vee B$ by disjunction introduction

---

(2) Accept Double Negation Elimination as a rule of inference and Reduce to Absurdity.

• $(C\to A)~\land ~(\neg C\to B)$ by premise.
  • $\neg(A\vee B)$ by assumption
    • $C$ by assumption
    • yadayadayadah.
    • $\bot$ by reasons
  • $\neg C$ by negation introduction
  • $\neg C\to B$ by conjunction elimination (simplification)
  • $B$ by conditional elimination (modus ponens)
  • $A\vee B$ by disjunction introduction
  • $\bot$ by negation elimination (sometimes called "contradiction introduction")
• $\neg\neg (A\vee B)$ by negation introduction
• $A\vee B$ by double negation elimination