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 φ
Assertion olci ψ φ

Proof

Step Hyp Ref Expression
1 orci.1 φ
2 1 a1i ¬ ψ φ
3 2 orri ψ φ