Theorem orcd 738

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

Syntax hints:   → wi 4   ∨ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  739  pm2.47  745  orim12i  764  animorl  828  animorrl  831  dcor  941  dfifp2dc  987  undif3ss  3466  dcun  3602  rabsnifsb  3735  exmidn0m  4289  exmidsssn  4290  reg2exmidlema  4630  acexmidlem1  6009  poxp  6392  nntri2or2  6661  nnm00  6693  ssfilem  7057  ssfilemd  7059  diffitest  7071  tridc  7084  finexdc  7087  elssdc  7089  fientri3  7102  unsnfidcex  7107  unsnfidcel  7108  fidcenumlemrks  7146  nninfisollem0  7323  nninfisollemeq  7325  finomni  7333  pr1or2  7393  exmidfodomrlemeldju  7403  exmidfodomrlemreseldju  7404  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  exmidaclem  7416  exmidontriimlem2  7430  netap  7466  2omotaplemap  7469  nqprloc  7758  mullocprlem  7783  recexprlemloc  7844  ltxrlt  8238  zmulcl  9526  nn0lt2  9554  zeo  9578  xrltso  10024  xnn0dcle  10030  xnn0letri  10031  apbtwnz  10527  expnegap0  10802  fzowrddc  11221  xrmaxadd  11815  zsumdc  11938  fsumsplit  11961  sumsplitdc  11986  isumlessdc  12050  zproddc  12133  fprodsplitdc  12150  fprodsplit  12151  fprodunsn  12158  fprodcl2lem  12159  prm23ge5  12830  pcxqcl  12878  gsum0g  13472  lringuplu  14203  suplociccreex  15341  lgsdir2lem5  15754  usgredg2v  16068  djulclALT  16347  trilpolemres  16596  trirec0  16598  nconstwlpolem0  16617  nconstwlpolem  16619