Theorem re1axmp

Description: ax-mp derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	re1axmp.min	$$⊢\phi$$
	re1axmp.maj	$$⊢\phi \to \psi$$
Assertion	re1axmp	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		re1axmp.min	$$⊢\phi$$
2		re1axmp.maj	$$⊢\phi \to \psi$$
3		rb-imdf	$$⊢\neg \left(\neg \left(\neg \left(\phi \to \psi \right)\vee \left(\neg \phi \vee \psi \right)\right)\vee \neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \left(\phi \to \psi \right)\right)\right)$$
4	3	rblem6	$$⊢\left(\neg \left(\phi \to \psi \right)\vee \left(\neg \phi \vee \psi \right)\right)$$
5	2 4	anmp	$$⊢\left(\neg \phi \vee \psi \right)$$
6	1 5	anmp	$$⊢\psi$$