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

Metamath Proof Explorer

Theorem imori

Description: Infer disjunction from implication. (Contributed by NM, 12-Mar-2012)

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

Step	Hyp	Ref	Expression
1		imori.1	$⊢ φ \to ψ$
2		imor	$⊢ (φ \to ψ) \leftrightarrow (\neg φ \lor ψ)$
3	1 2	mpbi	$⊢ (\neg φ \lor ψ)$