Theorem olcd 735

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

Syntax hints:   → wi 4   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  742  pm2.49  743  orim12i  760  pm1.5  766  animorr  825  animorlr  826  dcor  937  dcfrompeirce  1468  dcun  3569  exmidn0m  4244  regexmidlem1  4580  reg2exmidlema  4581  nn0suc  4651  nndceq0  4665  acexmidlem1  5939  nntri3or  6578  nntri2or2  6583  nndceq  6584  nndcel  6585  nnm00  6615  ssfilem  6971  diffitest  6983  tridc  6995  finexdc  6998  fientri3  7011  unsnfidcex  7016  unsnfidcel  7017  fidcenumlemrks  7054  fidcenumlemrk  7055  nninfisollemne  7232  nninfisol  7234  finomni  7241  exmidfodomrlemeldju  7306  exmidfodomrlemreseldju  7307  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  exmidaclem  7319  exmidontriimlem2  7333  netap  7365  2omotaplemap  7368  mullocprlem  7682  recexprlemloc  7743  gt0ap0  8698  ltap  8705  recexaplem2  8724  nn1m1nn  9053  nn1gt1  9069  ltpnf  9901  mnflt  9904  xrltso  9917  xnn0dcle  9923  xnn0letri  9924  xrpnfdc  9963  xrmnfdc  9964  exfzdc  10367  infssuzex  10374  apbtwnz  10415  expnnval  10685  exp0  10686  bc0k  10899  bcpasc  10909  ccatsymb  11056  xrmaxadd  11543  sumdc  11640  zsumdc  11666  fsum3  11669  fisumss  11674  isumss2  11675  fsumsplit  11689  zproddc  11861  fprodseq  11865  fprodssdc  11872  fprodsplitdc  11878  fprodsplit  11879  fprodunsn  11886  fprodcl2lem  11887  fsumdvds  12124  pclemdc  12582  pcxqcl  12606  sumhashdc  12641  1arith  12661  4sqlem17  12701  ctiunctlemudc  12779  lringuplu  13929  suplociccreex  15067  plymullem1  15191  lgsdir2lem5  15480  djurclALT  15700  bj-nn0suc0  15848  trilpolemres  15943  trirec0  15945  nconstwlpolem  15966