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

Metamath Proof Explorer

Theorem ornld

Description: Selecting one statement from a disjunction if one of the disjuncted statements is false. (Contributed by AV, 6-Sep-2018) (Proof shortened by AV, 13-Oct-2018) (Proof shortened by Wolf Lammen, 19-Jan-2020)

		Ref	Expression
	Assertion	ornld	⊢ ( 𝜑 → ( ( ( 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		pm3.35	⊢ ( ( 𝜑 ∧ ( 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ) → ( 𝜃 ∨ 𝜏 ) )
2	1	ord	⊢ ( ( 𝜑 ∧ ( 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ) → ( ¬ 𝜃 → 𝜏 ) )
3	2	expimpd	⊢ ( 𝜑 → ( ( ( 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )