Theorem orcd 728

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

Syntax hints:   → wi 4   ∨ wo 703

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  729  pm2.47  735  orim12i  754  animorl  818  animorrl  821  dcor  930  undif3ss  3388  dcun  3525  exmidn0m  4187  exmidsssn  4188  reg2exmidlema  4518  acexmidlem1  5849  poxp  6211  nntri2or2  6477  nnm00  6509  ssfilem  6853  diffitest  6865  tridc  6877  finexdc  6880  fientri3  6892  unsnfidcex  6897  unsnfidcel  6898  fidcenumlemrks  6930  nninfisollem0  7106  nninfisollemeq  7108  finomni  7116  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  exmidontriimlem2  7199  nqprloc  7507  mullocprlem  7532  recexprlemloc  7593  ltxrlt  7985  zmulcl  9265  nn0lt2  9293  zeo  9317  xrltso  9753  xnn0dcle  9759  xnn0letri  9760  apbtwnz  10230  expnegap0  10484  xrmaxadd  11224  zsumdc  11347  fsumsplit  11370  sumsplitdc  11395  isumlessdc  11459  zproddc  11542  fprodsplitdc  11559  fprodsplit  11560  fprodunsn  11567  fprodcl2lem  11568  prm23ge5  12218  suplociccreex  13396  lgsdir2lem5  13727  djulclALT  13836  trilpolemres  14074  trirec0  14076  nconstwlpolem0  14094  nconstwlpolem  14096