Metamath Proof Explorer

Theorem imorri

Description: Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypothesis imorri.1 
|- ( -. ph \/ ps )
Assertion imorri 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 imorri.1 
 |-  ( -. ph \/ ps )
2 imor 
 |-  ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
3 1 2 mpbir 
 |-  ( ph -> ps )