Metamath Proof Explorer

Theorem ralralimp

Description: Selecting one of two alternatives within a restricted generalization if one of the alternatives is false. (Contributed by AV, 6-Sep-2018) (Proof shortened by AV, 13-Oct-2018)

		Ref	Expression
	Assertion	ralralimp	$⊢ (φ \land A \neq \emptyset) \to (\forall x \in A ((φ \to (θ \lor τ)) \land \neg θ) \to τ)$

Proof

Step	Hyp	Ref	Expression
1		ornld	$⊢ φ \to (((φ \to (θ \lor τ)) \land \neg θ) \to τ)$
2	1	adantr	$⊢ (φ \land A \neq \emptyset) \to (((φ \to (θ \lor τ)) \land \neg θ) \to τ)$
3	2	ralimdv	$⊢ (φ \land A \neq \emptyset) \to (\forall x \in A ((φ \to (θ \lor τ)) \land \neg θ) \to \forall x \in A τ)$
4		rspn0	$⊢ A \neq \emptyset \to (\forall x \in A τ \to τ)$
5	4	adantl	$⊢ (φ \land A \neq \emptyset) \to (\forall x \in A τ \to τ)$
6	3 5	syld	$⊢ (φ \land A \neq \emptyset) \to (\forall x \in A ((φ \to (θ \lor τ)) \land \neg θ) \to τ)$