Theorem orcd 734

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 713	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  735  pm2.47  741  orim12i  760  animorl  824  animorrl  827  dcor  937  undif3ss  3425  dcun  3561  exmidn0m  4235  exmidsssn  4236  reg2exmidlema  4571  acexmidlem1  5921  poxp  6299  nntri2or2  6565  nnm00  6597  ssfilem  6945  diffitest  6957  tridc  6969  finexdc  6972  fientri3  6985  unsnfidcex  6990  unsnfidcel  6991  fidcenumlemrks  7028  nninfisollem0  7205  nninfisollemeq  7207  finomni  7215  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  exmidontriimlem2  7305  netap  7337  2omotaplemap  7340  nqprloc  7629  mullocprlem  7654  recexprlemloc  7715  ltxrlt  8109  zmulcl  9396  nn0lt2  9424  zeo  9448  xrltso  9888  xnn0dcle  9894  xnn0letri  9895  apbtwnz  10381  expnegap0  10656  xrmaxadd  11443  zsumdc  11566  fsumsplit  11589  sumsplitdc  11614  isumlessdc  11678  zproddc  11761  fprodsplitdc  11778  fprodsplit  11779  fprodunsn  11786  fprodcl2lem  11787  prm23ge5  12458  pcxqcl  12506  gsum0g  13098  lringuplu  13828  suplociccreex  14944  lgsdir2lem5  15357  djulclALT  15531  trilpolemres  15773  trirec0  15775  nconstwlpolem0  15794  nconstwlpolem  15796