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  4284  regexmidlem1  4624  reg2exmidlema  4625  nn0suc  4695  nndceq0  4709  acexmidlem1  5996  nntri3or  6637  nntri2or2  6642  nndceq  6643  nndcel  6644  nnm00  6674  ssfilem  7033  diffitest  7045  tridc  7057  finexdc  7060  fientri3  7073  unsnfidcex  7078  unsnfidcel  7079  fidcenumlemrks  7116  fidcenumlemrk  7117  nninfisollemne  7294  nninfisol  7296  finomni  7303  pr1or2  7363  exmidfodomrlemeldju  7373  exmidfodomrlemreseldju  7374  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidaclem  7386  exmidontriimlem2  7400  netap  7436  2omotaplemap  7439  mullocprlem  7753  recexprlemloc  7814  gt0ap0  8769  ltap  8776  recexaplem2  8795  nn1m1nn  9124  nn1gt1  9140  ltpnf  9972  mnflt  9975  xrltso  9988  xnn0dcle  9994  xnn0letri  9995  xrpnfdc  10034  xrmnfdc  10035  exfzdc  10441  infssuzex  10448  apbtwnz  10489  expnnval  10759  exp0  10760  bc0k  10973  bcpasc  10983  ccatsymb  11132  xrmaxadd  11767  sumdc  11864  zsumdc  11890  fsum3  11893  fisumss  11898  isumss2  11899  fsumsplit  11913  zproddc  12085  fprodseq  12089  fprodssdc  12096  fprodsplitdc  12102  fprodsplit  12103  fprodunsn  12110  fprodcl2lem  12111  fsumdvds  12348  pclemdc  12806  pcxqcl  12830  sumhashdc  12865  1arith  12885  4sqlem17  12925  ctiunctlemudc  13003  lringuplu  14154  suplociccreex  15292  plymullem1  15416  lgsdir2lem5  15705  umgrvad2edg  16003  djurclALT  16124  bj-nn0suc0  16271  trilpolemres  16369  trirec0  16371  nconstwlpolem  16392