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  3396  dcun  3533  exmidn0m  4198  exmidsssn  4199  reg2exmidlema  4530  acexmidlem1  5865  poxp  6227  nntri2or2  6493  nnm00  6525  ssfilem  6869  diffitest  6881  tridc  6893  finexdc  6896  fientri3  6908  unsnfidcex  6913  unsnfidcel  6914  fidcenumlemrks  6946  nninfisollem0  7122  nninfisollemeq  7124  finomni  7132  exmidfodomrlemeldju  7192  exmidfodomrlemreseldju  7193  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  exmidaclem  7201  exmidontriimlem2  7215  netap  7243  2omotaplemap  7246  nqprloc  7532  mullocprlem  7557  recexprlemloc  7618  ltxrlt  8010  zmulcl  9292  nn0lt2  9320  zeo  9344  xrltso  9780  xnn0dcle  9786  xnn0letri  9787  apbtwnz  10257  expnegap0  10511  xrmaxadd  11250  zsumdc  11373  fsumsplit  11396  sumsplitdc  11421  isumlessdc  11485  zproddc  11568  fprodsplitdc  11585  fprodsplit  11586  fprodunsn  11593  fprodcl2lem  11594  prm23ge5  12244  suplociccreex  13766  lgsdir2lem5  14097  djulclALT  14206  trilpolemres  14443  trirec0  14445  nconstwlpolem0  14463  nconstwlpolem  14465