Theorem orcd 685

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 666	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  olcd  686  pm2.47  692  orim12i  709  dcor  877  undif3ss  3241  reg2exmidlema  4305  acexmidlem1  5559  poxp  5904  nntri2or2  6162  nnm00  6189  ssfilem  6431  diffitest  6443  fientri3  6459  unsnfidcex  6464  unsnfidcel  6465  nqprloc  6849  mullocprlem  6874  recexprlemloc  6935  ltxrlt  7297  zmulcl  8537  nn0lt2  8562  zeo  8585  xrltso  8999  apbtwnz  9408  expnegap0  9633