Metamath Proof Explorer
Description: Deduction introducing a disjunct. (Contributed by NM, 19Jan2008)
(Proof shortened by Wolf Lammen, 14Nov2012)


Ref 
Expression 

Hypothesis 
orci.1 
$${\u22a2}{\phi}$$ 

Assertion 
olci 
$${\u22a2}\left({\psi}\vee {\phi}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

orci.1 
$${\u22a2}{\phi}$$ 
2 
1

a1i 
$${\u22a2}\neg {\psi}\to {\phi}$$ 
3 
2

orri 
$${\u22a2}\left({\psi}\vee {\phi}\right)$$ 