Theorem olcd 736

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

Syntax hints:   → wi 4   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  743  pm2.49  744  orim12i  761  pm1.5  767  animorr  826  animorlr  827  dcor  938  dcfrompeirce  1470  dcun  3574  exmidn0m  4253  regexmidlem1  4589  reg2exmidlema  4590  nn0suc  4660  nndceq0  4674  acexmidlem1  5953  nntri3or  6592  nntri2or2  6597  nndceq  6598  nndcel  6599  nnm00  6629  ssfilem  6987  diffitest  6999  tridc  7011  finexdc  7014  fientri3  7027  unsnfidcex  7032  unsnfidcel  7033  fidcenumlemrks  7070  fidcenumlemrk  7071  nninfisollemne  7248  nninfisol  7250  finomni  7257  pr1or2  7316  exmidfodomrlemeldju  7323  exmidfodomrlemreseldju  7324  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  exmidaclem  7336  exmidontriimlem2  7350  netap  7386  2omotaplemap  7389  mullocprlem  7703  recexprlemloc  7764  gt0ap0  8719  ltap  8726  recexaplem2  8745  nn1m1nn  9074  nn1gt1  9090  ltpnf  9922  mnflt  9925  xrltso  9938  xnn0dcle  9944  xnn0letri  9945  xrpnfdc  9984  xrmnfdc  9985  exfzdc  10391  infssuzex  10398  apbtwnz  10439  expnnval  10709  exp0  10710  bc0k  10923  bcpasc  10933  ccatsymb  11081  xrmaxadd  11647  sumdc  11744  zsumdc  11770  fsum3  11773  fisumss  11778  isumss2  11779  fsumsplit  11793  zproddc  11965  fprodseq  11969  fprodssdc  11976  fprodsplitdc  11982  fprodsplit  11983  fprodunsn  11990  fprodcl2lem  11991  fsumdvds  12228  pclemdc  12686  pcxqcl  12710  sumhashdc  12745  1arith  12765  4sqlem17  12805  ctiunctlemudc  12883  lringuplu  14033  suplociccreex  15171  plymullem1  15295  lgsdir2lem5  15584  djurclALT  15877  bj-nn0suc0  16024  trilpolemres  16122  trirec0  16124  nconstwlpolem  16145