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 ( ( 𝜑𝐴 ≠ ∅ ) → ( ∀ 𝑥𝐴 ( ( 𝜑 → ( 𝜃𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )

Proof

Step Hyp Ref Expression
1 ornld ( 𝜑 → ( ( ( 𝜑 → ( 𝜃𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )
2 1 adantr ( ( 𝜑𝐴 ≠ ∅ ) → ( ( ( 𝜑 → ( 𝜃𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )
3 2 ralimdv ( ( 𝜑𝐴 ≠ ∅ ) → ( ∀ 𝑥𝐴 ( ( 𝜑 → ( 𝜃𝜏 ) ) ∧ ¬ 𝜃 ) → ∀ 𝑥𝐴 𝜏 ) )
4 rspn0 ( 𝐴 ≠ ∅ → ( ∀ 𝑥𝐴 𝜏𝜏 ) )
5 4 adantl ( ( 𝜑𝐴 ≠ ∅ ) → ( ∀ 𝑥𝐴 𝜏𝜏 ) )
6 3 5 syld ( ( 𝜑𝐴 ≠ ∅ ) → ( ∀ 𝑥𝐴 ( ( 𝜑 → ( 𝜃𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )