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	⊢ 𝜑
	re1axmp.maj	⊢ ( 𝜑 → 𝜓 )
Assertion	re1axmp	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		re1axmp.min	⊢ 𝜑
2		re1axmp.maj	⊢ ( 𝜑 → 𝜓 )
3		rb-imdf	⊢ ¬ ( ¬ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) ∨ ¬ ( ¬ ( ¬ 𝜑 ∨ 𝜓 ) ∨ ( 𝜑 → 𝜓 ) ) )
4	3	rblem6	⊢ ( ¬ ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜑 ∨ 𝜓 ) )
5	2 4	anmp	⊢ ( ¬ 𝜑 ∨ 𝜓 )
6	1 5	anmp	⊢ 𝜓