Theorem orci 721

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 702	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 ∨ 𝜓)

Syntax hints:   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  truorfal  1385  prid1g  3659  onsucelsucexmidlem1  4481  regexmidlemm  4485  nn0suc  4557  nndceq0  4571  0elnn  4572  acexmidlem2  5811  exmidaclem  7122  indpi  7241  sup3exmid  8807  nn1gt1  8846  nneoor  9245  mnfltpnf  9670  bcpasc  10617  dceqnconst  13571  nconstwlpolem0  13574