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

Metamath Proof Explorer

Theorem 3ornot23

Description: If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		idd	$⊢ \neg φ \to (χ \to χ)$
2		pm2.21	$⊢ \neg φ \to (φ \to χ)$
3		pm2.21	$⊢ \neg ψ \to (ψ \to χ)$
4	1 2 3	3jaao	$⊢ (\neg φ \land \neg φ \land \neg ψ) \to ((χ \lor φ \lor ψ) \to χ)$
5	4	3anidm12	$⊢ (\neg φ \land \neg ψ) \to ((χ \lor φ \lor ψ) \to χ)$