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 )