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 ( 𝜑 → ( ( ( 𝜑 → ( 𝜃𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )

Proof

Step Hyp Ref Expression
1 pm3.35 ( ( 𝜑 ∧ ( 𝜑 → ( 𝜃𝜏 ) ) ) → ( 𝜃𝜏 ) )
2 1 ord ( ( 𝜑 ∧ ( 𝜑 → ( 𝜃𝜏 ) ) ) → ( ¬ 𝜃𝜏 ) )
3 2 expimpd ( 𝜑 → ( ( ( 𝜑 → ( 𝜃𝜏 ) ) ∧ ¬ 𝜃 ) → 𝜏 ) )