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  4340  regexmidlem1  4682  reg2exmidlema  4683  nn0suc  4753  nndceq0  4767  acexmidlem1  6084  nntri3or  6771  nntri2or2  6776  nndceq  6777  nndcel  6778  nnm00  6808  ssfilem  7183  ssfilemd  7185  diffitest  7197  tridc  7210  finexdc  7213  elssdc  7215  eqsndc  7216  fientri3  7228  unsnfidcex  7233  unsnfidcel  7234  fidcenumlemrks  7277  fidcenumlemrk  7278  nninfisollemne  7477  nninfisol  7479  finomni  7486  pr1or2  7546  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  exmidontriimlem2  7584  netap  7626  2omotaplemap  7629  mullocprlem  7943  recexprlemloc  8004  gt0ap0  8962  ltap  8969  recexaplem2  8988  nn1m1nn  9331  nn1gt1  9347  ltpnf  10198  mnflt  10201  xrltso  10214  xnn0dcle  10220  xnn0letri  10221  xrpnfdc  10260  xrmnfdc  10261  exfzdc  10675  infssuzex  10682  apbtwnz  10725  expnnval  10999  exp0  11000  resq01  11115  bc0k  11215  bcpasc  11225  ccatsymb  11391  xrmaxadd  12051  sumdc  12148  zsumdc  12175  fsum3  12178  fisumss  12183  isumss2  12184  fsumsplit  12198  zproddc  12370  fprodseq  12374  fprodssdc  12381  fprodsplitdc  12387  fprodsplit  12388  fprodunsn  12395  fprodcl2lem  12396  fsumdvds  12633  prmdcz  12933  pclemdc  13095  pcxqcl  13119  sumhashdc  13154  1arith  13174  4sqlem17  13214  ctiunctlemudc  13385  gsummptfidmsplit  14253  lringuplu  14611  aprlring  14708  suplociccreex  15867  plymullem1  15991  prmorcht  16299  lgsdir2lem5  16373  upgr1een  16587  umgrvad2edg  16674  usgr1e  16704  eupth2lem2dc  16922  eupth2lem3lem4fi  16936  dichmul0orlem3  16977  dichmul0orlem7  16981  djurclALT  17052  bj-nn0suc0  17198  trilpolemres  17315  trirec0  17317  nconstwlpolem  17339