Theorem orcd 734

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

Syntax hints:   → wi 4   ∨ wo 709

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  735  pm2.47  741  orim12i  760  animorl  824  animorrl  827  dcor  937  undif3ss  3420  dcun  3556  exmidn0m  4230  exmidsssn  4231  reg2exmidlema  4566  acexmidlem1  5914  poxp  6285  nntri2or2  6551  nnm00  6583  ssfilem  6931  diffitest  6943  tridc  6955  finexdc  6958  fientri3  6971  unsnfidcex  6976  unsnfidcel  6977  fidcenumlemrks  7012  nninfisollem0  7189  nninfisollemeq  7191  finomni  7199  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  exmidontriimlem2  7282  netap  7314  2omotaplemap  7317  nqprloc  7605  mullocprlem  7630  recexprlemloc  7691  ltxrlt  8085  zmulcl  9370  nn0lt2  9398  zeo  9422  xrltso  9862  xnn0dcle  9868  xnn0letri  9869  apbtwnz  10343  expnegap0  10618  xrmaxadd  11404  zsumdc  11527  fsumsplit  11550  sumsplitdc  11575  isumlessdc  11639  zproddc  11722  fprodsplitdc  11739  fprodsplit  11740  fprodunsn  11747  fprodcl2lem  11748  prm23ge5  12402  pcxqcl  12450  gsum0g  12979  lringuplu  13692  suplociccreex  14778  lgsdir2lem5  15148  djulclALT  15293  trilpolemres  15532  trirec0  15534  nconstwlpolem0  15553  nconstwlpolem  15555