This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orri

Description: Infer disjunction from implication. (Contributed by NM, 11-Jun-1994)

		Ref	Expression
	Hypothesis	orri.1	$⊢ \neg φ \to ψ$
	Assertion	orri	$⊢ (φ \lor ψ)$

Step	Hyp	Ref	Expression
1		orri.1	$⊢ \neg φ \to ψ$
2		df-or	$⊢ (φ \lor ψ) \leftrightarrow (\neg φ \to ψ)$
3	1 2	mpbir	$⊢ (φ \lor ψ)$