Theorem rbsyl

Description: Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rbsyl.1	$$⊢\left(\neg \psi \vee \chi \right)$$
	rbsyl.2	$$⊢\left(\phi \vee \psi \right)$$
Assertion	rbsyl	$$⊢\left(\phi \vee \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rbsyl.1	$$⊢\left(\neg \psi \vee \chi \right)$$
2		rbsyl.2	$$⊢\left(\phi \vee \psi \right)$$
3		rb-ax1	$$⊢\left(\neg \left(\neg \psi \vee \chi \right)\vee \left(\neg \left(\phi \vee \psi \right)\vee \left(\phi \vee \chi \right)\right)\right)$$
4	1 3	anmp	$$⊢\left(\neg \left(\phi \vee \psi \right)\vee \left(\phi \vee \chi \right)\right)$$
5	2 4	anmp	$$⊢\left(\phi \vee \chi \right)$$