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  3606  exmidn0m  4297  regexmidlem1  4637  reg2exmidlema  4638  nn0suc  4708  nndceq0  4722  acexmidlem1  6024  nntri3or  6704  nntri2or2  6709  nndceq  6710  nndcel  6711  nnm00  6741  ssfilem  7105  ssfilemd  7107  diffitest  7119  tridc  7132  finexdc  7135  elssdc  7137  eqsndc  7138  fientri3  7150  unsnfidcex  7155  unsnfidcel  7156  fidcenumlemrks  7195  fidcenumlemrk  7196  nninfisollemne  7373  nninfisol  7375  finomni  7382  pr1or2  7442  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  exmidontriimlem2  7480  netap  7516  2omotaplemap  7519  mullocprlem  7833  recexprlemloc  7894  gt0ap0  8848  ltap  8855  recexaplem2  8874  nn1m1nn  9203  nn1gt1  9219  ltpnf  10059  mnflt  10062  xrltso  10075  xnn0dcle  10081  xnn0letri  10082  xrpnfdc  10121  xrmnfdc  10122  exfzdc  10532  infssuzex  10539  apbtwnz  10580  expnnval  10850  exp0  10851  bc0k  11064  bcpasc  11074  ccatsymb  11228  xrmaxadd  11884  sumdc  11981  zsumdc  12008  fsum3  12011  fisumss  12016  isumss2  12017  fsumsplit  12031  zproddc  12203  fprodseq  12207  fprodssdc  12214  fprodsplitdc  12220  fprodsplit  12221  fprodunsn  12228  fprodcl2lem  12229  fsumdvds  12466  pclemdc  12924  pcxqcl  12948  sumhashdc  12983  1arith  13003  4sqlem17  13043  ctiunctlemudc  13121  lringuplu  14274  suplociccreex  15418  plymullem1  15542  lgsdir2lem5  15834  upgr1een  16048  umgrvad2edg  16135  usgr1e  16165  eupth2lem2dc  16383  eupth2lem3lem4fi  16397  djurclALT  16503  bj-nn0suc0  16649  trilpolemres  16757  trirec0  16759  nconstwlpolem  16781