Theorem orci 731

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

Syntax hints:   ∨ wo 708

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  truorfal  1406  prid1g  3698  onsucelsucexmidlem1  4529  regexmidlemm  4533  nn0suc  4605  nndceq0  4619  0elnn  4620  acexmidlem2  5874  dcfi  6982  exmidaclem  7209  indpi  7343  sup3exmid  8916  nn1gt1  8955  nneoor  9357  mnfltpnf  9787  bcpasc  10748  dceqnconst  14893  nconstwlpolem0  14896