Theorem olcd 746

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.48  753  pm2.49  754  orim12i  771  pm1.5  777  animorr  836  animorlr  837  dcor  948  dfifp2dc  994  dcfrompeirce  1499  dcun  3637  exmidn0m  4338  regexmidlem1  4680  reg2exmidlema  4681  nn0suc  4751  nndceq0  4765  acexmidlem1  6081  nntri3or  6766  nntri2or2  6771  nndceq  6772  nndcel  6773  nnm00  6803  ssfilem  7177  ssfilemd  7179  diffitest  7191  tridc  7204  finexdc  7207  elssdc  7209  eqsndc  7210  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  fidcenumlemrks  7270  fidcenumlemrk  7271  nninfisollemne  7471  nninfisol  7473  finomni  7480  pr1or2  7540  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem2  7578  netap  7620  2omotaplemap  7623  mullocprlem  7937  recexprlemloc  7998  gt0ap0  8954  ltap  8961  recexaplem2  8980  nn1m1nn  9322  nn1gt1  9338  ltpnf  10182  mnflt  10185  xrltso  10198  xnn0dcle  10204  xnn0letri  10205  xrpnfdc  10244  xrmnfdc  10245  exfzdc  10659  infssuzex  10666  apbtwnz  10709  expnnval  10979  exp0  10980  resq01  11095  bc0k  11194  bcpasc  11204  ccatsymb  11370  xrmaxadd  12027  sumdc  12124  zsumdc  12151  fsum3  12154  fisumss  12159  isumss2  12160  fsumsplit  12174  zproddc  12346  fprodseq  12350  fprodssdc  12357  fprodsplitdc  12363  fprodsplit  12364  fprodunsn  12371  fprodcl2lem  12372  fsumdvds  12609  pclemdc  13067  pcxqcl  13091  sumhashdc  13126  1arith  13146  4sqlem17  13186  ctiunctlemudc  13328  lringuplu  14503  aprlring  14600  suplociccreex  15725  plymullem1  15849  lgsdir2lem5  16151  upgr1een  16365  umgrvad2edg  16452  usgr1e  16482  eupth2lem2dc  16700  eupth2lem3lem4fi  16714  dichmul0orlem3  16755  dichmul0orlem7  16759  djurclALT  16830  bj-nn0suc0  16976  trilpolemres  17091  trirec0  17093  nconstwlpolem  17115