Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR ( \/ insertion right), see natded . (Contributed by NM, 20-Sep-2007)
Ref | Expression | ||
---|---|---|---|
Hypothesis | orcd.1 | |
|
Assertion | orcd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcd.1 | |
|
2 | orc | |
|
3 | 1 2 | syl | |