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  4621  regexmidlemm  4625  nn0suc  4697  nndceq0  4711  0elnn  4712  acexmidlem2  6007  dcfi  7164  exmidaclem  7406  indpi  7545  sup3exmid  9120  nn1gt1  9160  nneoor  9565  mnfltpnf  9998  bcpasc  11005  usgrexmpldifpr  16068  dceqnconst  16542  nconstwlpolem0  16545