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  7471  nninfisollemeq  7473  finomni  7481  pr1or2  7541  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  exmidontriimlem2  7579  netap  7621  2omotaplemap  7624  nqprloc  7913  mullocprlem  7938  recexprlemloc  7999  ltxrlt  8392  zmulcl  9703  nn0lt2  9732  zeo  9756  xrltso  10209  xnn0dcle  10215  xnn0letri  10216  apbtwnz  10720  expnegap0  10998  resq01  11109  fzowrddc  11434  xrmaxadd  12045  zsumdc  12169  fsumsplit  12192  sumsplitdc  12217  isumlessdc  12281  zproddc  12364  fprodsplitdc  12381  fprodsplit  12382  fprodunsn  12389  fprodcl2lem  12390  prm23ge5  13065  pcxqcl  13113  gzsum0  13764  lringuplu  14554  aprlring  14651  suplociccreex  15777  lgsdir2lem5  16273  usgredg2v  16587  dichmul0orlem3  16877  dichmul0orlem7  16881  djulclALT  16951  trilpolemres  17213  trirec0  17215  nconstwlpolem0  17235  nconstwlpolem  17237