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  3602  exmidn0m  4289  regexmidlem1  4629  reg2exmidlema  4630  nn0suc  4700  nndceq0  4714  acexmidlem1  6009  nntri3or  6656  nntri2or2  6661  nndceq  6662  nndcel  6663  nnm00  6693  ssfilem  7057  diffitest  7069  tridc  7082  finexdc  7085  elssdc  7087  eqsndc  7088  fientri3  7100  unsnfidcex  7105  unsnfidcel  7106  fidcenumlemrks  7143  fidcenumlemrk  7144  nninfisollemne  7321  nninfisol  7323  finomni  7330  pr1or2  7390  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  exmidontriimlem2  7427  netap  7463  2omotaplemap  7466  mullocprlem  7780  recexprlemloc  7841  gt0ap0  8796  ltap  8803  recexaplem2  8822  nn1m1nn  9151  nn1gt1  9167  ltpnf  10005  mnflt  10008  xrltso  10021  xnn0dcle  10027  xnn0letri  10028  xrpnfdc  10067  xrmnfdc  10068  exfzdc  10476  infssuzex  10483  apbtwnz  10524  expnnval  10794  exp0  10795  bc0k  11008  bcpasc  11018  ccatsymb  11169  xrmaxadd  11812  sumdc  11909  zsumdc  11935  fsum3  11938  fisumss  11943  isumss2  11944  fsumsplit  11958  zproddc  12130  fprodseq  12134  fprodssdc  12141  fprodsplitdc  12147  fprodsplit  12148  fprodunsn  12155  fprodcl2lem  12156  fsumdvds  12393  pclemdc  12851  pcxqcl  12875  sumhashdc  12910  1arith  12930  4sqlem17  12970  ctiunctlemudc  13048  lringuplu  14200  suplociccreex  15338  plymullem1  15462  lgsdir2lem5  15751  umgrvad2edg  16050  usgr1e  16080  djurclALT  16334  bj-nn0suc0  16481  trilpolemres  16582  trirec0  16584  nconstwlpolem  16605