Theorem orcd 745

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  pm2.47  752  orim12i  771  animorl  835  animorrl  838  dcor  948  dfifp2dc  994  undif3ss  3492  dcun  3637  ifeqeqxdc  3687  rabsnifsb  3777  exmidn0m  4338  exmidsssn  4339  reg2exmidlema  4681  acexmidlem1  6081  poxp  6468  nntri2or2  6771  nnm00  6803  ssfilem  7177  ssfilemd  7179  diffitest  7191  tridc  7204  finexdc  7207  elssdc  7209  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  fidcenumlemrks  7270  fdcf1  7316  nninfisollem0  7470  nninfisollemeq  7472  finomni  7480  pr1or2  7540  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem2  7578  netap  7620  2omotaplemap  7623  nqprloc  7912  mullocprlem  7937  recexprlemloc  7998  ltxrlt  8391  zmulcl  9700  nn0lt2  9729  zeo  9753  xrltso  10200  xnn0dcle  10206  xnn0letri  10207  apbtwnz  10711  expnegap0  10986  resq01  11097  fzowrddc  11421  xrmaxadd  12029  zsumdc  12153  fsumsplit  12176  sumsplitdc  12201  isumlessdc  12265  zproddc  12348  fprodsplitdc  12365  fprodsplit  12366  fprodunsn  12373  fprodcl2lem  12374  prm23ge5  13045  pcxqcl  13093  gzsum0  13715  lringuplu  14505  aprlring  14602  suplociccreex  15727  lgsdir2lem5  16163  usgredg2v  16477  dichmul0orlem3  16767  dichmul0orlem7  16771  djulclALT  16841  trilpolemres  17103  trirec0  17105  nconstwlpolem0  17125  nconstwlpolem  17127