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  9648  nn0lt2  9677  zeo  9701  xrltso  10148  xnn0dcle  10154  xnn0letri  10155  apbtwnz  10658  expnegap0  10933  resq01  11044  fzowrddc  11364  xrmaxadd  11971  zsumdc  12095  fsumsplit  12118  sumsplitdc  12143  isumlessdc  12207  zproddc  12290  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodcl2lem  12316  prm23ge5  12987  pcxqcl  13035  gsum0g  13693  lringuplu  14426  aprlring  14523  suplociccreex  15601  lgsdir2lem5  16017  usgredg2v  16331  djulclALT  16685  trilpolemres  16938  trirec0  16940  trimul0or  16957  nconstwlpolem0  16961  nconstwlpolem  16963