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  3465  dcun  3601  exmidn0m  4284  exmidsssn  4285  reg2exmidlema  4623  acexmidlem1  5990  poxp  6368  nntri2or2  6634  nnm00  6666  ssfilem  7025  diffitest  7037  tridc  7049  finexdc  7052  fientri3  7065  unsnfidcex  7070  unsnfidcel  7071  fidcenumlemrks  7108  nninfisollem0  7285  nninfisollemeq  7287  finomni  7295  pr1or2  7355  exmidfodomrlemeldju  7365  exmidfodomrlemreseldju  7366  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  exmidaclem  7378  exmidontriimlem2  7392  netap  7428  2omotaplemap  7431  nqprloc  7720  mullocprlem  7745  recexprlemloc  7806  ltxrlt  8200  zmulcl  9488  nn0lt2  9516  zeo  9540  xrltso  9980  xnn0dcle  9986  xnn0letri  9987  apbtwnz  10481  expnegap0  10756  fzowrddc  11165  xrmaxadd  11758  zsumdc  11881  fsumsplit  11904  sumsplitdc  11929  isumlessdc  11993  zproddc  12076  fprodsplitdc  12093  fprodsplit  12094  fprodunsn  12101  fprodcl2lem  12102  prm23ge5  12773  pcxqcl  12821  gsum0g  13415  lringuplu  14145  suplociccreex  15283  lgsdir2lem5  15696  usgredg2v  16007  djulclALT  16095  trilpolemres  16341  trirec0  16343  nconstwlpolem0  16362  nconstwlpolem  16364