Theorem olcd 746

Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
orcd.1	|- ( ph -> ps )

Assertion

Ref	Expression
olcd	|- ( ph -> ( ch \/ ps ) )

Proof of Theorem olcd

Step	Hyp	Ref	Expression
1		orcd.1	. . 3 |- ( ph -> ps )
2	1	orcd 745	. 2 |- ( ph -> ( ps \/ ch ) )
3	2	orcomd 741	1 |- ( ph -> ( ch \/ ps ) )

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-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.48  753  pm2.49  754  orim12i  771  pm1.5  777  animorr  836  animorlr  837  dcor  948  dfifp2dc  994  dcfrompeirce  1499  dcun  3637  exmidn0m  4340  regexmidlem1  4682  reg2exmidlema  4683  nn0suc  4753  nndceq0  4767  acexmidlem1  6084  nntri3or  6770  nntri2or2  6775  nndceq  6776  nndcel  6777  nnm00  6807  ssfilem  7181  ssfilemd  7183  diffitest  7195  tridc  7208  finexdc  7211  elssdc  7213  eqsndc  7214  fientri3  7226  unsnfidcex  7231  unsnfidcel  7232  fidcenumlemrks  7275  fidcenumlemrk  7276  nninfisollemne  7477  nninfisol  7479  finomni  7486  pr1or2  7546  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  exmidontriimlem2  7584  netap  7626  2omotaplemap  7629  mullocprlem  7943  recexprlemloc  8004  gt0ap0  8962  ltap  8969  recexaplem2  8988  nn1m1nn  9331  nn1gt1  9347  ltpnf  10199  mnflt  10202  xrltso  10215  xnn0dcle  10221  xnn0letri  10222  xrpnfdc  10261  xrmnfdc  10262  exfzdc  10676  infssuzex  10683  apbtwnz  10726  expnnval  11000  exp0  11001  resq01  11116  bc0k  11216  bcpasc  11226  ccatsymb  11392  xrmaxadd  12052  sumdc  12149  zsumdc  12176  fsum3  12179  fisumss  12184  isumss2  12185  fsumsplit  12199  zproddc  12371  fprodseq  12375  fprodssdc  12382  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcl2lem  12397  fsumdvds  12634  prmdcz  12934  pclemdc  13096  pcxqcl  13120  sumhashdc  13155  1arith  13175  4sqlem17  13215  ctiunctlemudc  13386  gsummptfidmsplit  14254  lringuplu  14612  aprlring  14709  suplociccreex  15850  plymullem1  15974  prmorcht  16282  lgsdir2lem5  16356  upgr1een  16570  umgrvad2edg  16657  usgr1e  16687  eupth2lem2dc  16905  eupth2lem3lem4fi  16919  dichmul0orlem3  16960  dichmul0orlem7  16964  djurclALT  17035  bj-nn0suc0  17181  trilpolemres  17298  trirec0  17300  nconstwlpolem  17322