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 
orci 
$${\u22a2}\left({\phi}\vee {\psi}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

pm2.24i 
$${\u22a2}\neg {\phi}\to {\psi}$$ 
3 
2

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