Theorem orcd 722

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

Syntax hints:   → wi 4   ∨ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  723  pm2.47  729  orim12i  748  dcor  919  undif3ss  3332  dcun  3468  exmidn0m  4119  exmidsssn  4120  reg2exmidlema  4444  acexmidlem1  5763  poxp  6122  nntri2or2  6387  nnm00  6418  ssfilem  6762  diffitest  6774  tridc  6786  finexdc  6789  fientri3  6796  unsnfidcex  6801  unsnfidcel  6802  fidcenumlemrks  6834  finomni  7005  exmidfodomrlemeldju  7048  exmidfodomrlemreseldju  7049  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  nqprloc  7346  mullocprlem  7371  recexprlemloc  7432  ltxrlt  7823  zmulcl  9100  nn0lt2  9125  zeo  9149  xrltso  9575  apbtwnz  10040  expnegap0  10294  xrmaxadd  11023  zsumdc  11146  fsumsplit  11169  sumsplitdc  11194  isumlessdc  11258  suplociccreex  12760  djulclALT  12997  trilpolemres  13224