Metamath Proof Explorer

Theorem orci

Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008) (Proof shortened by Wolf Lammen, 14-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 orci.1 
 |-  ph
2 1 pm2.24i 
 |-  ( -. ph -> ps )
3 2 orri 
 |-  ( ph \/ ps )