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

Metamath Proof Explorer

Theorem 3orel13

Description: Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011)

		Ref	Expression
	Assertion	3orel13	$⊢ (\neg φ \land \neg χ) \to ((φ \lor ψ \lor χ) \to ψ)$

Step	Hyp	Ref	Expression
1		3orel3	$⊢ \neg χ \to ((φ \lor ψ \lor χ) \to (φ \lor ψ))$
2		orel1	$⊢ \neg φ \to ((φ \lor ψ) \to ψ)$
3	1 2	sylan9r	$⊢ (\neg φ \land \neg χ) \to ((φ \lor ψ \lor χ) \to ψ)$