Theorem orcd 745

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  pm2.47  752  orim12i  771  animorl  835  animorrl  838  dcor  948  dfifp2dc  994  undif3ss  3492  dcun  3637  ifeqeqxdc  3687  rabsnifsb  3777  exmidn0m  4340  exmidsssn  4341  reg2exmidlema  4683  acexmidlem1  6084  poxp  6472  nntri2or2  6776  nnm00  6808  ssfilem  7183  ssfilemd  7185  diffitest  7197  tridc  7210  finexdc  7213  elssdc  7215  fientri3  7228  unsnfidcex  7233  unsnfidcel  7234  fidcenumlemrks  7277  fdcf1  7322  nninfisollem0  7477  nninfisollemeq  7479  finomni  7487  pr1or2  7547  exmidfodomrlemeldju  7558  exmidfodomrlemreseldju  7559  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidaclem  7571  exmidontriimlem2  7585  netap  7627  2omotaplemap  7630  nqprloc  7919  mullocprlem  7944  recexprlemloc  8005  ltxrlt  8398  zmulcl  9708  nn0lt2  9737  zeo  9762  xrltso  10215  xnn0dcle  10221  xnn0letri  10222  apbtwnz  10726  expnegap0  11005  resq01  11116  fzowrddc  11441  xrmaxadd  12052  zsumdc  12176  fsumsplit  12199  sumsplitdc  12224  isumlessdc  12288  zproddc  12371  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcl2lem  12397  prm23ge5  13072  pcxqcl  13120  gzsum0  13772  lringuplu  14612  aprlring  14709  suplociccreex  15883  lgsdir2lem5  16389  usgredg2v  16703  dichmul0orlem3  16993  dichmul0orlem7  16997  djulclALT  17067  trilpolemres  17331  trirec0  17333  nconstwlpolem0  17353  nconstwlpolem  17355