Are you talking about natural deduction and specifically about the following rule (taken from the book "Proofs and Types," p. 72)?

Do I understand right that there are three formulas above the line: (q v r), and two (p ^ q) v (p ^ q)? Then you get it from the rule above by having A = q, B = r and C = (p ^ q) v (p ^ q).

Originally Posted by

**ssharish** But the following i'n not sure how the [V-elmi] would yield to (q v r) from (p ^ q) v (p v r).

I don't see p v r. Also, why do you say "yield to (q v r) from ..."? The formula q v r is above the line, so one uses it as an assumption to yield the conclusion below the line.

Hint: To write things that require alignment, you can use the [code]...[/code] tags, which don't turn a sequence of spaces into a single space. Write what you want in a text editor *using a fixed-width font* like Courier New or Consolas and then paste it into the browser's text edit box. For example, you can have

Code:

(q v r) (p ^ q) v (p ^ q) (p ^ q) v (p ^ q)
--------------------------------------------------- [v-elmi]
(p ^ q) v (p ^ q)