Theorem orcd 684

Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)

Hypothesis

Ref	Expression
orcd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
orcd	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2 ⊢ (𝜑 → 𝜓)
2		orc 665	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  olcd  685  pm2.47  691  orim12i  708  dcor  876  undif3ss  3225  reg2exmidlema  4277  acexmidlem1  5528  poxp  5873  nntri2or2  6099  nnm00  6125  ssfilem  6360  diffitest  6371  fientri3  6381  unsnfidcex  6385  unsnfidcel  6386  nqprloc  6735  mullocprlem  6760  recexprlemloc  6821  ltxrlt  7178  zmulcl  8404  nn0lt2  8429  zeo  8452  xrltso  8871  expnegap0  9484