Theorem orcd 741

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

Syntax hints:   → wi 4   ∨ wo 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  742  pm2.47  748  orim12i  767  animorl  831  animorrl  834  dcor  944  dfifp2dc  990  undif3ss  3470  dcun  3606  rabsnifsb  3741  exmidn0m  4297  exmidsssn  4298  reg2exmidlema  4638  acexmidlem1  6024  poxp  6406  nntri2or2  6709  nnm00  6741  ssfilem  7105  ssfilemd  7107  diffitest  7119  tridc  7132  finexdc  7135  elssdc  7137  fientri3  7150  unsnfidcex  7155  unsnfidcel  7156  fidcenumlemrks  7195  nninfisollem0  7372  nninfisollemeq  7374  finomni  7382  pr1or2  7442  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  exmidontriimlem2  7480  netap  7516  2omotaplemap  7519  nqprloc  7808  mullocprlem  7833  recexprlemloc  7894  ltxrlt  8288  zmulcl  9576  nn0lt2  9604  zeo  9628  xrltso  10074  xnn0dcle  10080  xnn0letri  10081  apbtwnz  10578  expnegap0  10853  fzowrddc  11275  xrmaxadd  11882  zsumdc  12006  fsumsplit  12029  sumsplitdc  12054  isumlessdc  12118  zproddc  12201  fprodsplitdc  12218  fprodsplit  12219  fprodunsn  12226  fprodcl2lem  12227  prm23ge5  12898  pcxqcl  12946  gsum0g  13540  lringuplu  14272  suplociccreex  15415  lgsdir2lem5  15831  usgredg2v  16145  djulclALT  16499  trilpolemres  16754  trirec0  16756  nconstwlpolem0  16776  nconstwlpolem  16778