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  7472  nninfisol  7474  finomni  7481  pr1or2  7541  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  exmidontriimlem2  7579  netap  7621  2omotaplemap  7624  mullocprlem  7938  recexprlemloc  7999  gt0ap0  8957  ltap  8964  recexaplem2  8983  nn1m1nn  9325  nn1gt1  9341  ltpnf  10193  mnflt  10196  xrltso  10209  xnn0dcle  10215  xnn0letri  10216  xrpnfdc  10255  xrmnfdc  10256  exfzdc  10670  infssuzex  10677  apbtwnz  10720  expnnval  10994  exp0  10995  resq01  11110  bc0k  11210  bcpasc  11220  ccatsymb  11386  xrmaxadd  12046  sumdc  12143  zsumdc  12170  fsum3  12173  fisumss  12178  isumss2  12179  fsumsplit  12193  zproddc  12365  fprodseq  12369  fprodssdc  12376  fprodsplitdc  12382  fprodsplit  12383  fprodunsn  12390  fprodcl2lem  12391  fsumdvds  12628  prmdcz  12928  pclemdc  13090  pcxqcl  13114  sumhashdc  13149  1arith  13169  4sqlem17  13209  ctiunctlemudc  13380  lringuplu  14587  aprlring  14684  suplociccreex  15816  plymullem1  15940  prmorcht  16243  lgsdir2lem5  16317  upgr1een  16531  umgrvad2edg  16618  usgr1e  16648  eupth2lem2dc  16866  eupth2lem3lem4fi  16880  dichmul0orlem3  16921  dichmul0orlem7  16925  djurclALT  16996  bj-nn0suc0  17142  trilpolemres  17258  trirec0  17260  nconstwlpolem  17282