Theorem olcd 724

Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
orcd.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem olcd

Step	Hyp	Ref	Expression
1		orcd.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	orcd 723	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	2	orcomd 719	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-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.48  731  pm2.49  732  orim12i  749  pm1.5  755  animorr  814  animorlr  815  dcan  923  dcor  925  dcun  3519  exmidn0m  4180  regexmidlem1  4510  reg2exmidlema  4511  nn0suc  4581  nndceq0  4595  acexmidlem1  5838  nntri3or  6461  nntri2or2  6466  nndceq  6467  nndcel  6468  nnm00  6497  ssfilem  6841  diffitest  6853  tridc  6865  finexdc  6868  fientri3  6880  unsnfidcex  6885  unsnfidcel  6886  fidcenumlemrks  6918  fidcenumlemrk  6919  nninfisollemne  7095  nninfisol  7097  finomni  7104  exmidfodomrlemeldju  7155  exmidfodomrlemreseldju  7156  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  exmidontriimlem2  7178  mullocprlem  7511  recexprlemloc  7572  gt0ap0  8524  ltap  8531  recexaplem2  8549  nn1m1nn  8875  nn1gt1  8891  ltpnf  9716  mnflt  9719  xrltso  9732  xnn0dcle  9738  xnn0letri  9739  xrpnfdc  9778  xrmnfdc  9779  exfzdc  10175  apbtwnz  10209  expnnval  10458  exp0  10459  bc0k  10669  bcpasc  10679  xrmaxadd  11202  sumdc  11299  zsumdc  11325  fsum3  11328  fisumss  11333  isumss2  11334  fsumsplit  11348  zproddc  11520  fprodseq  11524  fprodssdc  11531  fprodsplitdc  11537  fprodsplit  11538  fprodunsn  11545  fprodcl2lem  11546  infssuzex  11882  pclemdc  12220  sumhashdc  12277  1arith  12297  ctiunctlemudc  12370  suplociccreex  13252  lgsdir2lem5  13583  djurclALT  13693  bj-nn0suc0  13842  trilpolemres  13931  trirec0  13933  nconstwlpolem  13953