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	$⊢ φ \to (((φ \to (θ \lor τ)) \land \neg θ) \to τ)$

Proof

Step	Hyp	Ref	Expression
1		pm3.35	$⊢ (φ \land (φ \to (θ \lor τ))) \to (θ \lor τ)$
2	1	ord	$⊢ (φ \land (φ \to (θ \lor τ))) \to (\neg θ \to τ)$
3	2	expimpd	$⊢ φ \to (((φ \to (θ \lor τ)) \land \neg θ) \to τ)$