Theorem orci 736

Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
orci.1	⊢ 𝜑

Assertion

Ref	Expression
orci	⊢ (𝜑 ∨ 𝜓)

Proof of Theorem orci

Step	Hyp	Ref	Expression
1		orci.1	. 2 ⊢ 𝜑
2		orc 717	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ wo 713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1448  prid1g  3770  onsucelsucexmidlem1  4620  regexmidlemm  4624  nn0suc  4696  nndceq0  4710  0elnn  4711  acexmidlem2  6004  dcfi  7156  exmidaclem  7398  indpi  7537  sup3exmid  9112  nn1gt1  9152  nneoor  9557  mnfltpnf  9989  bcpasc  10996  dceqnconst  16458  nconstwlpolem0  16461