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  6013  nntri3or  6660  nntri2or2  6665  nndceq  6666  nndcel  6667  nnm00  6697  ssfilem  7061  ssfilemd  7063  diffitest  7075  tridc  7088  finexdc  7091  elssdc  7093  eqsndc  7094  fientri3  7106  unsnfidcex  7111  unsnfidcel  7112  fidcenumlemrks  7151  fidcenumlemrk  7152  nninfisollemne  7329  nninfisol  7331  finomni  7338  pr1or2  7398  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  exmidontriimlem2  7436  netap  7472  2omotaplemap  7475  mullocprlem  7789  recexprlemloc  7850  gt0ap0  8805  ltap  8812  recexaplem2  8831  nn1m1nn  9160  nn1gt1  9176  ltpnf  10014  mnflt  10017  xrltso  10030  xnn0dcle  10036  xnn0letri  10037  xrpnfdc  10076  xrmnfdc  10077  exfzdc  10485  infssuzex  10492  apbtwnz  10533  expnnval  10803  exp0  10804  bc0k  11017  bcpasc  11027  ccatsymb  11178  xrmaxadd  11821  sumdc  11918  zsumdc  11944  fsum3  11947  fisumss  11952  isumss2  11953  fsumsplit  11967  zproddc  12139  fprodseq  12143  fprodssdc  12150  fprodsplitdc  12156  fprodsplit  12157  fprodunsn  12164  fprodcl2lem  12165  fsumdvds  12402  pclemdc  12860  pcxqcl  12884  sumhashdc  12919  1arith  12939  4sqlem17  12979  ctiunctlemudc  13057  lringuplu  14209  suplociccreex  15347  plymullem1  15471  lgsdir2lem5  15760  upgr1een  15974  umgrvad2edg  16061  usgr1e  16091  eupth2lem2dc  16309  djurclALT  16398  bj-nn0suc0  16545  trilpolemres  16646  trirec0  16648  nconstwlpolem  16669