Theorem orcd 740

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

Syntax hints:   → wi 4   ∨ wo 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  741  pm2.47  747  orim12i  766  animorl  830  animorrl  833  dcor  943  dfifp2dc  989  undif3ss  3468  dcun  3604  rabsnifsb  3737  exmidn0m  4291  exmidsssn  4292  reg2exmidlema  4632  acexmidlem1  6014  poxp  6397  nntri2or2  6666  nnm00  6698  ssfilem  7062  ssfilemd  7064  diffitest  7076  tridc  7089  finexdc  7092  elssdc  7094  fientri3  7107  unsnfidcex  7112  unsnfidcel  7113  fidcenumlemrks  7152  nninfisollem0  7329  nninfisollemeq  7331  finomni  7339  pr1or2  7399  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem2  7437  netap  7473  2omotaplemap  7476  nqprloc  7765  mullocprlem  7790  recexprlemloc  7851  ltxrlt  8245  zmulcl  9533  nn0lt2  9561  zeo  9585  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  apbtwnz  10535  expnegap0  10810  fzowrddc  11232  xrmaxadd  11826  zsumdc  11950  fsumsplit  11973  sumsplitdc  11998  isumlessdc  12062  zproddc  12145  fprodsplitdc  12162  fprodsplit  12163  fprodunsn  12170  fprodcl2lem  12171  prm23ge5  12842  pcxqcl  12890  gsum0g  13484  lringuplu  14216  suplociccreex  15354  lgsdir2lem5  15767  usgredg2v  16081  djulclALT  16423  trilpolemres  16672  trirec0  16674  nconstwlpolem0  16693  nconstwlpolem  16695