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 φ A x A φ θ τ ¬ θ τ

Proof

Step Hyp Ref Expression
1 ornld φ φ θ τ ¬ θ τ
2 1 adantr φ A φ θ τ ¬ θ τ
3 2 ralimdv φ A x A φ θ τ ¬ θ x A τ
4 rspn0 A x A τ τ
5 4 adantl φ A x A τ τ
6 3 5 syld φ A x A φ θ τ ¬ θ τ