Theorem olcd 742

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 741	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	2	orcomd 737	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  749  pm2.49  750  orim12i  767  pm1.5  773  animorr  832  animorlr  833  dcor  944  dfifp2dc  990  dcfrompeirce  1495  dcun  3624  exmidn0m  4320  regexmidlem1  4662  reg2exmidlema  4663  nn0suc  4733  nndceq0  4747  acexmidlem1  6056  nntri3or  6741  nntri2or2  6746  nndceq  6747  nndcel  6748  nnm00  6778  ssfilem  7145  ssfilemd  7147  diffitest  7159  tridc  7172  finexdc  7175  elssdc  7177  eqsndc  7178  fientri3  7190  unsnfidcex  7195  unsnfidcel  7196  fidcenumlemrks  7238  fidcenumlemrk  7239  nninfisollemne  7437  nninfisol  7439  finomni  7446  pr1or2  7506  exmidfodomrlemeldju  7517  exmidfodomrlemreseldju  7518  exmidfodomrlemr  7520  exmidfodomrlemrALT  7521  exmidaclem  7530  exmidontriimlem2  7544  netap  7586  2omotaplemap  7589  mullocprlem  7903  recexprlemloc  7964  gt0ap0  8920  ltap  8927  recexaplem2  8946  nn1m1nn  9277  nn1gt1  9293  ltpnf  10137  mnflt  10140  xrltso  10153  xnn0dcle  10159  xnn0letri  10160  xrpnfdc  10199  xrmnfdc  10200  exfzdc  10613  infssuzex  10620  apbtwnz  10663  expnnval  10933  exp0  10934  resq01  11049  bc0k  11148  bcpasc  11158  ccatsymb  11320  xrmaxadd  11977  sumdc  12074  zsumdc  12101  fsum3  12104  fisumss  12109  isumss2  12110  fsumsplit  12124  zproddc  12296  fprodseq  12300  fprodssdc  12307  fprodsplitdc  12313  fprodsplit  12314  fprodunsn  12321  fprodcl2lem  12322  fsumdvds  12559  pclemdc  13017  pcxqcl  13041  sumhashdc  13076  1arith  13096  4sqlem17  13136  ctiunctlemudc  13278  lringuplu  14448  aprlring  14545  suplociccreex  15620  plymullem1  15744  lgsdir2lem5  16036  upgr1een  16250  umgrvad2edg  16337  usgr1e  16367  eupth2lem2dc  16585  eupth2lem3lem4fi  16599  dichmul0orlem3  16640  dichmul0orlem7  16644  djurclALT  16715  bj-nn0suc0  16861  trilpolemres  16967  trirec0  16969  nconstwlpolem  16991