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	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		idd	⊢ ( ¬ 𝜑 → ( 𝜒 → 𝜒 ) )
2		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜒 ) )
3		pm2.21	⊢ ( ¬ 𝜓 → ( 𝜓 → 𝜒 ) )
4	1 2 3	3jaao	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜑 ∧ ¬ 𝜓 ) → ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) → 𝜒 ) )
5	4	3anidm12	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) → 𝜒 ) )