Theorem orcd 738

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

Syntax hints:   → wi 4   ∨ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  739  pm2.47  745  orim12i  764  animorl  828  animorrl  831  dcor  941  dfifp2dc  987  undif3ss  3465  dcun  3601  exmidn0m  4286  exmidsssn  4287  reg2exmidlema  4627  acexmidlem1  6006  poxp  6389  nntri2or2  6657  nnm00  6689  ssfilem  7050  diffitest  7062  tridc  7075  finexdc  7078  elssdc  7080  fientri3  7093  unsnfidcex  7098  unsnfidcel  7099  fidcenumlemrks  7136  nninfisollem0  7313  nninfisollemeq  7315  finomni  7323  pr1or2  7383  exmidfodomrlemeldju  7393  exmidfodomrlemreseldju  7394  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  exmidaclem  7406  exmidontriimlem2  7420  netap  7456  2omotaplemap  7459  nqprloc  7748  mullocprlem  7773  recexprlemloc  7834  ltxrlt  8228  zmulcl  9516  nn0lt2  9544  zeo  9568  xrltso  10009  xnn0dcle  10015  xnn0letri  10016  apbtwnz  10511  expnegap0  10786  fzowrddc  11200  xrmaxadd  11793  zsumdc  11916  fsumsplit  11939  sumsplitdc  11964  isumlessdc  12028  zproddc  12111  fprodsplitdc  12128  fprodsplit  12129  fprodunsn  12136  fprodcl2lem  12137  prm23ge5  12808  pcxqcl  12856  gsum0g  13450  lringuplu  14181  suplociccreex  15319  lgsdir2lem5  15732  usgredg2v  16043  djulclALT  16274  trilpolemres  16524  trirec0  16526  nconstwlpolem0  16545  nconstwlpolem  16547