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  3424  dcun  3560  exmidn0m  4234  exmidsssn  4235  reg2exmidlema  4570  acexmidlem1  5918  poxp  6290  nntri2or2  6556  nnm00  6588  ssfilem  6936  diffitest  6948  tridc  6960  finexdc  6963  fientri3  6976  unsnfidcex  6981  unsnfidcel  6982  fidcenumlemrks  7019  nninfisollem0  7196  nninfisollemeq  7198  finomni  7206  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  exmidontriimlem2  7289  netap  7321  2omotaplemap  7324  nqprloc  7612  mullocprlem  7637  recexprlemloc  7698  ltxrlt  8092  zmulcl  9379  nn0lt2  9407  zeo  9431  xrltso  9871  xnn0dcle  9877  xnn0letri  9878  apbtwnz  10364  expnegap0  10639  xrmaxadd  11426  zsumdc  11549  fsumsplit  11572  sumsplitdc  11597  isumlessdc  11661  zproddc  11744  fprodsplitdc  11761  fprodsplit  11762  fprodunsn  11769  fprodcl2lem  11770  prm23ge5  12433  pcxqcl  12481  gsum0g  13039  lringuplu  13752  suplociccreex  14860  lgsdir2lem5  15273  djulclALT  15447  trilpolemres  15686  trirec0  15688  nconstwlpolem0  15707  nconstwlpolem  15709