Metamath Proof Explorer

Theorem olci

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 olci 
|- ( ps \/ ph )

Proof

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