Theorem olcd 742

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

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  749  pm2.49  750  orim12i  767  pm1.5  773  animorr  832  animorlr  833  dcor  944  dfifp2dc  990  dcfrompeirce  1495  dcun  3619  exmidn0m  4314  regexmidlem1  4655  reg2exmidlema  4656  nn0suc  4726  nndceq0  4740  acexmidlem1  6046  nntri3or  6726  nntri2or2  6731  nndceq  6732  nndcel  6733  nnm00  6763  ssfilem  7130  ssfilemd  7132  diffitest  7144  tridc  7157  finexdc  7160  elssdc  7162  eqsndc  7163  fientri3  7175  unsnfidcex  7180  unsnfidcel  7181  fidcenumlemrks  7223  fidcenumlemrk  7224  nninfisollemne  7422  nninfisol  7424  finomni  7431  pr1or2  7491  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  exmidontriimlem2  7529  netap  7568  2omotaplemap  7571  mullocprlem  7885  recexprlemloc  7946  gt0ap0  8900  ltap  8907  recexaplem2  8926  nn1m1nn  9255  nn1gt1  9271  ltpnf  10113  mnflt  10116  xrltso  10129  xnn0dcle  10135  xnn0letri  10136  xrpnfdc  10175  xrmnfdc  10176  exfzdc  10586  infssuzex  10593  apbtwnz  10634  expnnval  10904  exp0  10905  bc0k  11118  bcpasc  11128  ccatsymb  11290  xrmaxadd  11946  sumdc  12043  zsumdc  12070  fsum3  12073  fisumss  12078  isumss2  12079  fsumsplit  12093  zproddc  12265  fprodseq  12269  fprodssdc  12276  fprodsplitdc  12282  fprodsplit  12283  fprodunsn  12290  fprodcl2lem  12291  fsumdvds  12528  pclemdc  12986  pcxqcl  13010  sumhashdc  13045  1arith  13065  4sqlem17  13105  ctiunctlemudc  13188  lringuplu  14341  aprlring  14434  suplociccreex  15489  plymullem1  15613  lgsdir2lem5  15905  upgr1een  16119  umgrvad2edg  16206  usgr1e  16236  eupth2lem2dc  16454  eupth2lem3lem4fi  16468  djurclALT  16574  bj-nn0suc0  16720  trilpolemres  16826  trirec0  16828  trimul0or  16845  nconstwlpolem  16851