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	|- ph
	re1axmp.maj	|- ( ph -> ps )
Assertion	re1axmp	|- ps

Proof

Step	Hyp	Ref	Expression
1		re1axmp.min	|- ph
2		re1axmp.maj	|- ( ph -> ps )
3		rb-imdf	|- -. ( -. ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) ) \/ -. ( -. ( -. ph \/ ps ) \/ ( ph -> ps ) ) )
4	3	rblem6	|- ( -. ( ph -> ps ) \/ ( -. ph \/ ps ) )
5	2 4	anmp	|- ( -. ph \/ ps )
6	1 5	anmp	|- ps