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 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 720

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  746  pm2.47  752  orim12i  771  animorl  835  animorrl  838  dcor  948  dfifp2dc  994  undif3ss  3492  dcun  3637  ifeqeqxdc  3687  rabsnifsb  3776  exmidn0m  4336  exmidsssn  4337  reg2exmidlema  4679  acexmidlem1  6075  poxp  6462  nntri2or2  6765  nnm00  6797  ssfilem  7171  ssfilemd  7173  diffitest  7185  tridc  7198  finexdc  7201  elssdc  7203  fientri3  7216  unsnfidcex  7221  unsnfidcel  7222  fidcenumlemrks  7264  fdcf1  7310  nninfisollem0  7464  nninfisollemeq  7466  finomni  7474  pr1or2  7534  exmidfodomrlemeldju  7545  exmidfodomrlemreseldju  7546  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  exmidaclem  7558  exmidontriimlem2  7572  netap  7614  2omotaplemap  7617  nqprloc  7906  mullocprlem  7931  recexprlemloc  7992  ltxrlt  8385  zmulcl  9681  nn0lt2  9710  zeo  9734  xrltso  10181  xnn0dcle  10187  xnn0letri  10188  apbtwnz  10692  expnegap0  10967  resq01  11078  fzowrddc  11402  xrmaxadd  12010  zsumdc  12134  fsumsplit  12157  sumsplitdc  12182  isumlessdc  12246  zproddc  12329  fprodsplitdc  12346  fprodsplit  12347  fprodunsn  12354  fprodcl2lem  12355  prm23ge5  13026  pcxqcl  13074  gzsum0  13696  lringuplu  14486  aprlring  14583  suplociccreex  15708  lgsdir2lem5  16134  usgredg2v  16448  dichmul0orlem3  16738  dichmul0orlem7  16742  djulclALT  16812  trilpolemres  17065  trirec0  17067  nconstwlpolem0  17087  nconstwlpolem  17089