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	$$⊢\phi \to \left(\left(\left(\phi \to \left(\theta \vee \tau \right)\right)\wedge \neg \theta \right)\to \tau \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm3.35	$$⊢\left(\phi \wedge \left(\phi \to \left(\theta \vee \tau \right)\right)\right)\to \left(\theta \vee \tau \right)$$
2	1	ord	$$⊢\left(\phi \wedge \left(\phi \to \left(\theta \vee \tau \right)\right)\right)\to \left(\neg \theta \to \tau \right)$$
3	2	expimpd	$$⊢\phi \to \left(\left(\left(\phi \to \left(\theta \vee \tau \right)\right)\wedge \neg \theta \right)\to \tau \right)$$