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  3411  dcun  3548  exmidn0m  4219  exmidsssn  4220  reg2exmidlema  4551  acexmidlem1  5893  poxp  6258  nntri2or2  6524  nnm00  6556  ssfilem  6904  diffitest  6916  tridc  6928  finexdc  6931  fientri3  6944  unsnfidcex  6949  unsnfidcel  6950  fidcenumlemrks  6983  nninfisollem0  7159  nninfisollemeq  7161  finomni  7169  exmidfodomrlemeldju  7229  exmidfodomrlemreseldju  7230  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  exmidaclem  7238  exmidontriimlem2  7252  netap  7284  2omotaplemap  7287  nqprloc  7575  mullocprlem  7600  recexprlemloc  7661  ltxrlt  8054  zmulcl  9337  nn0lt2  9365  zeo  9389  xrltso  9828  xnn0dcle  9834  xnn0letri  9835  apbtwnz  10307  expnegap0  10562  xrmaxadd  11304  zsumdc  11427  fsumsplit  11450  sumsplitdc  11475  isumlessdc  11539  zproddc  11622  fprodsplitdc  11639  fprodsplit  11640  fprodunsn  11647  fprodcl2lem  11648  prm23ge5  12299  pcxqcl  12347  gsum0g  12874  lringuplu  13560  suplociccreex  14579  lgsdir2lem5  14911  djulclALT  15031  trilpolemres  15269  trirec0  15271  nconstwlpolem0  15290  nconstwlpolem  15292