Theorem orcd 723

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

Syntax hints:   → wi 4   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  724  pm2.47  730  orim12i  749  animorl  813  animorrl  816  dcor  925  undif3ss  3383  dcun  3519  exmidn0m  4180  exmidsssn  4181  reg2exmidlema  4511  acexmidlem1  5838  poxp  6200  nntri2or2  6466  nnm00  6497  ssfilem  6841  diffitest  6853  tridc  6865  finexdc  6868  fientri3  6880  unsnfidcex  6885  unsnfidcel  6886  fidcenumlemrks  6918  nninfisollem0  7094  nninfisollemeq  7096  finomni  7104  exmidfodomrlemeldju  7155  exmidfodomrlemreseldju  7156  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  exmidontriimlem2  7178  nqprloc  7486  mullocprlem  7511  recexprlemloc  7572  ltxrlt  7964  zmulcl  9244  nn0lt2  9272  zeo  9296  xrltso  9732  xnn0dcle  9738  xnn0letri  9739  apbtwnz  10209  expnegap0  10463  xrmaxadd  11202  zsumdc  11325  fsumsplit  11348  sumsplitdc  11373  isumlessdc  11437  zproddc  11520  fprodsplitdc  11537  fprodsplit  11538  fprodunsn  11545  fprodcl2lem  11546  prm23ge5  12196  suplociccreex  13242  lgsdir2lem5  13573  djulclALT  13682  trilpolemres  13921  trirec0  13923  nconstwlpolem0  13941  nconstwlpolem  13943