Theorem olcd 739

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  746  pm2.49  747  orim12i  764  pm1.5  770  animorr  829  animorlr  830  dcor  941  dfifp2dc  987  dcfrompeirce  1492  dcun  3601  exmidn0m  4285  regexmidlem1  4625  reg2exmidlema  4626  nn0suc  4696  nndceq0  4710  acexmidlem1  6003  nntri3or  6647  nntri2or2  6652  nndceq  6653  nndcel  6654  nnm00  6684  ssfilem  7045  diffitest  7057  tridc  7070  finexdc  7073  elssdc  7075  eqsndc  7076  fientri3  7088  unsnfidcex  7093  unsnfidcel  7094  fidcenumlemrks  7131  fidcenumlemrk  7132  nninfisollemne  7309  nninfisol  7311  finomni  7318  pr1or2  7378  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  exmidontriimlem2  7415  netap  7451  2omotaplemap  7454  mullocprlem  7768  recexprlemloc  7829  gt0ap0  8784  ltap  8791  recexaplem2  8810  nn1m1nn  9139  nn1gt1  9155  ltpnf  9988  mnflt  9991  xrltso  10004  xnn0dcle  10010  xnn0letri  10011  xrpnfdc  10050  xrmnfdc  10051  exfzdc  10458  infssuzex  10465  apbtwnz  10506  expnnval  10776  exp0  10777  bc0k  10990  bcpasc  11000  ccatsymb  11150  xrmaxadd  11787  sumdc  11884  zsumdc  11910  fsum3  11913  fisumss  11918  isumss2  11919  fsumsplit  11933  zproddc  12105  fprodseq  12109  fprodssdc  12116  fprodsplitdc  12122  fprodsplit  12123  fprodunsn  12130  fprodcl2lem  12131  fsumdvds  12368  pclemdc  12826  pcxqcl  12850  sumhashdc  12885  1arith  12905  4sqlem17  12945  ctiunctlemudc  13023  lringuplu  14175  suplociccreex  15313  plymullem1  15437  lgsdir2lem5  15726  umgrvad2edg  16024  djurclALT  16221  bj-nn0suc0  16368  trilpolemres  16470  trirec0  16472  nconstwlpolem  16493