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  11514  sumdc  11611  zsumdc  11637  fsum3  11640  fisumss  11645  isumss2  11646  fsumsplit  11660  zproddc  11832  fprodseq  11836  fprodssdc  11843  fprodsplitdc  11849  fprodsplit  11850  fprodunsn  11857  fprodcl2lem  11858  fsumdvds  12095  pclemdc  12553  pcxqcl  12577  sumhashdc  12612  1arith  12632  4sqlem17  12672  ctiunctlemudc  12750  lringuplu  13900  suplociccreex  15038  plymullem1  15162  lgsdir2lem5  15451  djurclALT  15671  bj-nn0suc0  15819  trilpolemres  15914  trirec0  15916  nconstwlpolem  15937