Theorem orcd 652

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

Syntax hints:   → wi 4   ∨ wo 629

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  olcd  653  pm2.47  659  orim12i  676  dcor  843  sspsstrir  3046  undif3ss  3198  reg2exmidlema  4259  acexmidlem1  5508  poxp  5853  nntri2or2  6076  nnm00  6102  ssfiexmid  6336  diffitest  6344  fientri3  6353  nqprloc  6643  mullocprlem  6668  recexprlemloc  6729  ltxrlt  7085  zmulcl  8297  nn0lt2  8322  zeo  8343  xrltso  8717  expnegap0  9263