Metamath Proof Explorer


Theorem orcd

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 φψχ

Proof

Step Hyp Ref Expression
1 orcd.1 φψ
2 orc ψψχ
3 1 2 syl φψχ