bv-∨

Theorem.

Arguments:

(pr), (pr), (sv),

Hypotheses:

( bound in )

( bound in )

Assertions:

( bound in ())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
		2	( bound in )
2	bv-¬	3	( bound in )
1, 3	bv-→	4	( bound in ())
	df-or	5	(()())
4, 5	bvdef	6	( bound in ())