Theorem olcd 723

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

Syntax hints:   → wi 4   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.48  730  pm2.49  731  orim12i  748  pm1.5  754  dcan  918  dcor  919  dcun  3468  exmidn0m  4119  regexmidlem1  4443  reg2exmidlema  4444  nn0suc  4513  nndceq0  4526  acexmidlem1  5763  nntri3or  6382  nntri2or2  6387  nndceq  6388  nndcel  6389  nnm00  6418  ssfilem  6762  diffitest  6774  tridc  6786  finexdc  6789  fientri3  6796  unsnfidcex  6801  unsnfidcel  6802  fidcenumlemrks  6834  fidcenumlemrk  6835  finomni  7005  exmidfodomrlemeldju  7048  exmidfodomrlemreseldju  7049  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  mullocprlem  7371  recexprlemloc  7432  gt0ap0  8381  ltap  8388  recexaplem2  8406  nn1m1nn  8731  nn1gt1  8747  ltpnf  9560  mnflt  9562  xrltso  9575  xrpnfdc  9618  xrmnfdc  9619  exfzdc  10010  apbtwnz  10040  expnnval  10289  exp0  10290  bc0k  10495  bcpasc  10505  xrmaxadd  11023  sumdc  11120  zsumdc  11146  fsum3  11149  fisumss  11154  isumss2  11155  fsumsplit  11169  infssuzex  11631  ctiunctlemudc  11939  suplociccreex  12760  djurclALT  12998  bj-nn0suc0  13137  trilpolemres  13224