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  4285  exmidsssn  4286  reg2exmidlema  4626  acexmidlem1  6003  poxp  6384  nntri2or2  6652  nnm00  6684  ssfilem  7045  diffitest  7057  tridc  7069  finexdc  7072  fientri3  7085  unsnfidcex  7090  unsnfidcel  7091  fidcenumlemrks  7128  nninfisollem0  7305  nninfisollemeq  7307  finomni  7315  pr1or2  7375  exmidfodomrlemeldju  7385  exmidfodomrlemreseldju  7386  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  exmidaclem  7398  exmidontriimlem2  7412  netap  7448  2omotaplemap  7451  nqprloc  7740  mullocprlem  7765  recexprlemloc  7826  ltxrlt  8220  zmulcl  9508  nn0lt2  9536  zeo  9560  xrltso  10000  xnn0dcle  10006  xnn0letri  10007  apbtwnz  10502  expnegap0  10777  fzowrddc  11187  xrmaxadd  11780  zsumdc  11903  fsumsplit  11926  sumsplitdc  11951  isumlessdc  12015  zproddc  12098  fprodsplitdc  12115  fprodsplit  12116  fprodunsn  12123  fprodcl2lem  12124  prm23ge5  12795  pcxqcl  12843  gsum0g  13437  lringuplu  14168  suplociccreex  15306  lgsdir2lem5  15719  usgredg2v  16030  djulclALT  16189  trilpolemres  16440  trirec0  16442  nconstwlpolem0  16461  nconstwlpolem  16463