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  4340  exmidsssn  4341  reg2exmidlema  4683  acexmidlem1  6084  poxp  6472  nntri2or2  6775  nnm00  6807  ssfilem  7182  ssfilemd  7184  diffitest  7196  tridc  7209  finexdc  7212  elssdc  7214  fientri3  7227  unsnfidcex  7232  unsnfidcel  7233  fidcenumlemrks  7276  fdcf1  7322  nninfisollem0  7477  nninfisollemeq  7479  finomni  7487  pr1or2  7547  exmidfodomrlemeldju  7558  exmidfodomrlemreseldju  7559  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidaclem  7571  exmidontriimlem2  7585  netap  7627  2omotaplemap  7630  nqprloc  7919  mullocprlem  7944  recexprlemloc  8005  ltxrlt  8398  zmulcl  9710  nn0lt2  9739  zeo  9763  xrltso  10216  xnn0dcle  10222  xnn0letri  10223  apbtwnz  10727  expnegap0  11006  resq01  11117  fzowrddc  11442  xrmaxadd  12053  zsumdc  12177  fsumsplit  12200  sumsplitdc  12225  isumlessdc  12289  zproddc  12372  fprodsplitdc  12389  fprodsplit  12390  fprodunsn  12397  fprodcl2lem  12398  prm23ge5  13073  pcxqcl  13121  gzsum0  13773  lringuplu  14613  aprlring  14710  suplociccreex  15862  lgsdir2lem5  16368  usgredg2v  16682  dichmul0orlem3  16972  dichmul0orlem7  16976  djulclALT  17046  trilpolemres  17310  trirec0  17312  nconstwlpolem0  17332  nconstwlpolem  17334