find formal proof Got stuck while figuring out the formal proof for the following:
$$\begin{array}{r}
A\lor B\\
\neg B\lor C\\
\hline
A\lor C
\end{array}$$
The conclusion seems obvious. But finding a formal proof for it does not seem to be a trivial task for me.
I am trying to solve it via the backwards method. The conclusion is most likely to be derived via $\lor$Elim rule, but I cannot figure out how to derive it from the premises.
I will be grateful for any hints! Thank you!
 A: It's been a long time, and I've forgotten the standard notation and terminology, but you can split up a disjunction (I think it's called "disjunction elimination", as you alluded to in the question) into two subproofs; if they have the same result, you can then claim that result:
$$\begin{array}{rcl}
1&A\lor B&\textrm{given}\\
2&\neg B\lor C&\textrm{given}\\
3&A&\textrm{assume}\\
3.1&A\lor C&\textrm{disjunction introduction, or whatever it's called, }3\\
4&B&\textrm{assume}\\
4.1&\neg\neg B&\textrm{whatever the rule's called, }4\\
4.2&C&\textrm{whatever the rule's called, }2,4.1\\
4.3&A\lor C&\textrm{disjunction introduction, or whatever it's called, }4.2\\
5&A\lor C&\textrm{disjunction elimination, or whatever it's called, }1,3.1,4.3\end{array}$$
A: I think you can do the subproof where you assume A and derive (A v C).  You can always re-assume any premise further in the scope lines if you really want to do so, or seems convenient.  So, the other subproof might look like this, with the numbering re-worked:
0 (¬B∨C) premise
1  |    B assumption
2  ||  ¬C assumption
3  ||| (¬B∨C) assumption
4  |||| ¬B assumption
5  |||| Contradiction (not sure how you write the symbol here) 1, 4

6  |||| C assumption
7  |||| Contradiction 2, 6
8  ||| Contradiction 3, 4-5, 6-7 V elimination
9  || ¬(¬B∨C) 3-8 ¬ introduction
10 || Contradiction 0, 9
11 | ¬¬C 2-11 ¬ introduction
12 | C 11 ¬ elimination
13 C 1-12, 0, and the other subproof 

Note, I'm not sure if Fitch will accept this exactly, as I've never used that program.  I also feel more confident that Fitch would accept the following distinct full proof:
1     (A v B) premise
2     (¬B∨C) premise
3  |   C  assumption
4  |  (A v C) 3 V introduction
5  |   ¬B assumption
6  ||  A assumption
7  ||  (A v C) 6 V introduction
8  ||  B assumption
9  ||| ¬(A v C) assumption
10 ||| Contradiction 5, 8
11 ||  ¬ ¬(A v C) 9-10 negation introduction
12 || (A v C) 11 negation elimination
13 |  (A v C) 1, 6-7, 8-12 disjunction elimination
14    (A v C) 2, 3-4, 5-13 V introduction.

Edit: I'm not sure if Fitch will accept "(A v C)", but it should come as a simple matter to drop the parentheses here.  Also, if Fitch doesn't accept "(A v C)", but does accept "A v C" this actually comes as a weakness of the program, since "A v C" is not what logicians have called a "well-formed formula", while "(A v C)" does qualify as one... though your text uses the term "well-formed formula" in a slightly different way than I have here.
A: The following proof uses disjunction elimination (vE) for both premises.

I consider case $A$ on lines 3-4 and case $B$ on lines 5-11 from the first premise. For case $B$, I consider the two cases from the second premise, $¬B$ and $C$.  On line 8, I use explosion (X) because of the contradiction obtained on line 7. 
Links to the proof checker and the forallx textbook are given below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
