Theorem orcd 735

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

Syntax hints:   → wi 4   ∨ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  736  pm2.47  742  orim12i  761  animorl  825  animorrl  828  dcor  938  undif3ss  3436  dcun  3572  exmidn0m  4250  exmidsssn  4251  reg2exmidlema  4587  acexmidlem1  5950  poxp  6328  nntri2or2  6594  nnm00  6626  ssfilem  6984  diffitest  6996  tridc  7008  finexdc  7011  fientri3  7024  unsnfidcex  7029  unsnfidcel  7030  fidcenumlemrks  7067  nninfisollem0  7244  nninfisollemeq  7246  finomni  7254  pr1or2  7313  exmidfodomrlemeldju  7320  exmidfodomrlemreseldju  7321  exmidfodomrlemr  7323  exmidfodomrlemrALT  7324  exmidaclem  7333  exmidontriimlem2  7347  netap  7379  2omotaplemap  7382  nqprloc  7671  mullocprlem  7696  recexprlemloc  7757  ltxrlt  8151  zmulcl  9439  nn0lt2  9467  zeo  9491  xrltso  9931  xnn0dcle  9937  xnn0letri  9938  apbtwnz  10430  expnegap0  10705  fzowrddc  11114  xrmaxadd  11622  zsumdc  11745  fsumsplit  11768  sumsplitdc  11793  isumlessdc  11857  zproddc  11940  fprodsplitdc  11957  fprodsplit  11958  fprodunsn  11965  fprodcl2lem  11966  prm23ge5  12637  pcxqcl  12685  gsum0g  13278  lringuplu  14008  suplociccreex  15146  lgsdir2lem5  15559  djulclALT  15851  trilpolemres  16096  trirec0  16098  nconstwlpolem0  16117  nconstwlpolem  16119