Theorem orcd 733

Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)

Hypothesis

Ref	Expression
orcd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
orcd	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2 ⊢ (𝜑 → 𝜓)
2		orc 712	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  734  pm2.47  740  orim12i  759  animorl  823  animorrl  826  dcor  935  undif3ss  3398  dcun  3535  exmidn0m  4203  exmidsssn  4204  reg2exmidlema  4535  acexmidlem1  5873  poxp  6235  nntri2or2  6501  nnm00  6533  ssfilem  6877  diffitest  6889  tridc  6901  finexdc  6904  fientri3  6916  unsnfidcex  6921  unsnfidcel  6922  fidcenumlemrks  6954  nninfisollem0  7130  nninfisollemeq  7132  finomni  7140  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  exmidontriimlem2  7223  netap  7255  2omotaplemap  7258  nqprloc  7546  mullocprlem  7571  recexprlemloc  7632  ltxrlt  8025  zmulcl  9308  nn0lt2  9336  zeo  9360  xrltso  9798  xnn0dcle  9804  xnn0letri  9805  apbtwnz  10276  expnegap0  10530  xrmaxadd  11271  zsumdc  11394  fsumsplit  11417  sumsplitdc  11442  isumlessdc  11506  zproddc  11589  fprodsplitdc  11606  fprodsplit  11607  fprodunsn  11614  fprodcl2lem  11615  prm23ge5  12266  lringuplu  13342  suplociccreex  14141  lgsdir2lem5  14472  djulclALT  14592  trilpolemres  14829  trirec0  14831  nconstwlpolem0  14849  nconstwlpolem  14851