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  3486  dcun  3623  ifeqeqxdc  3673  rabsnifsb  3762  exmidn0m  4319  exmidsssn  4320  reg2exmidlema  4661  acexmidlem1  6054  poxp  6441  nntri2or2  6744  nnm00  6776  ssfilem  7143  ssfilemd  7145  diffitest  7157  tridc  7170  finexdc  7173  elssdc  7175  fientri3  7188  unsnfidcex  7193  unsnfidcel  7194  fidcenumlemrks  7236  nninfisollem0  7434  nninfisollemeq  7436  finomni  7444  pr1or2  7504  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  exmidontriimlem2  7542  netap  7584  2omotaplemap  7587  nqprloc  7876  mullocprlem  7901  recexprlemloc  7962  ltxrlt  8355  zmulcl  9651  nn0lt2  9680  zeo  9704  xrltso  10151  xnn0dcle  10157  xnn0letri  10158  apbtwnz  10661  expnegap0  10936  resq01  11047  fzowrddc  11367  xrmaxadd  11975  zsumdc  12099  fsumsplit  12122  sumsplitdc  12147  isumlessdc  12211  zproddc  12294  fprodsplitdc  12311  fprodsplit  12312  fprodunsn  12319  fprodcl2lem  12320  prm23ge5  12991  pcxqcl  13039  gsum0g  13663  lringuplu  14445  aprlring  14542  suplociccreex  15619  lgsdir2lem5  16035  usgredg2v  16349  dichmul0orlem3  16639  dichmul0orlem7  16643  djulclALT  16713  trilpolemres  16966  trirec0  16968  nconstwlpolem0  16988  nconstwlpolem  16990