Metamath Proof Explorer


Theorem ori

Description: Infer implication from disjunction. (Contributed by NM, 11-Jun-1994)

Ref Expression
Hypothesis ori.1 ( 𝜑𝜓 )
Assertion ori ( ¬ 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 ori.1 ( 𝜑𝜓 )
2 df-or ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜓 ) )
3 1 2 mpbi ( ¬ 𝜑𝜓 )