Theorem olcd 741

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

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  748  pm2.49  749  orim12i  766  pm1.5  772  animorr  831  animorlr  832  dcor  943  dfifp2dc  989  dcfrompeirce  1494  dcun  3604  exmidn0m  4291  regexmidlem1  4631  reg2exmidlema  4632  nn0suc  4702  nndceq0  4716  acexmidlem1  6014  nntri3or  6661  nntri2or2  6666  nndceq  6667  nndcel  6668  nnm00  6698  ssfilem  7062  ssfilemd  7064  diffitest  7076  tridc  7089  finexdc  7092  elssdc  7094  eqsndc  7095  fientri3  7107  unsnfidcex  7112  unsnfidcel  7113  fidcenumlemrks  7152  fidcenumlemrk  7153  nninfisollemne  7330  nninfisol  7332  finomni  7339  pr1or2  7399  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem2  7437  netap  7473  2omotaplemap  7476  mullocprlem  7790  recexprlemloc  7851  gt0ap0  8806  ltap  8813  recexaplem2  8832  nn1m1nn  9161  nn1gt1  9177  ltpnf  10015  mnflt  10018  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  xrpnfdc  10077  xrmnfdc  10078  exfzdc  10487  infssuzex  10494  apbtwnz  10535  expnnval  10805  exp0  10806  bc0k  11019  bcpasc  11029  ccatsymb  11183  xrmaxadd  11826  sumdc  11923  zsumdc  11950  fsum3  11953  fisumss  11958  isumss2  11959  fsumsplit  11973  zproddc  12145  fprodseq  12149  fprodssdc  12156  fprodsplitdc  12162  fprodsplit  12163  fprodunsn  12170  fprodcl2lem  12171  fsumdvds  12408  pclemdc  12866  pcxqcl  12890  sumhashdc  12925  1arith  12945  4sqlem17  12985  ctiunctlemudc  13063  lringuplu  14216  suplociccreex  15354  plymullem1  15478  lgsdir2lem5  15767  upgr1een  15981  umgrvad2edg  16068  usgr1e  16098  eupth2lem2dc  16316  eupth2lem3lem4fi  16330  djurclALT  16424  bj-nn0suc0  16571  trilpolemres  16672  trirec0  16674  nconstwlpolem  16696