Theorem anmp 1676

Description: Modus ponens for \/ -. axiom systems. (Contributed by Anthony Hart, 12-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
anmp.min	|- ph
anmp.maj	|- ( -. ph \/ ps )

Assertion

Ref	Expression
anmp	|- ps

Proof of Theorem anmp

Step	Hyp	Ref	Expression
1		anmp.min	. 2 |- ph
2		anmp.maj	. . 3 |- ( -. ph \/ ps )
3	2	imorri 430	. 2 |- ( ph -> ps )
4	1, 3	ax-mp 5	1 |- ps

Syntax hints:   -. wn 3   \/ wo 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385

This theorem is referenced by:  rbsyl  1681  rblem1  1682  rblem2  1683  rblem4  1685  rblem5  1686  rblem6  1687  rblem7  1688  re1axmp  1689  re2luk1  1690  re2luk2  1691  re2luk3  1692