Theorem olcd 735

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 734	. 2 |- ( ph -> ( ps \/ ch ) )
3	2	orcomd 730	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  742  pm2.49  743  orim12i  760  pm1.5  766  animorr  825  animorlr  826  dcor  937  dcfrompeirce  1460  dcun  3560  exmidn0m  4234  regexmidlem1  4569  reg2exmidlema  4570  nn0suc  4640  nndceq0  4654  acexmidlem1  5918  nntri3or  6551  nntri2or2  6556  nndceq  6557  nndcel  6558  nnm00  6588  ssfilem  6936  diffitest  6948  tridc  6960  finexdc  6963  fientri3  6976  unsnfidcex  6981  unsnfidcel  6982  fidcenumlemrks  7019  fidcenumlemrk  7020  nninfisollemne  7197  nninfisol  7199  finomni  7206  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  exmidontriimlem2  7289  netap  7321  2omotaplemap  7324  mullocprlem  7637  recexprlemloc  7698  gt0ap0  8653  ltap  8660  recexaplem2  8679  nn1m1nn  9008  nn1gt1  9024  ltpnf  9855  mnflt  9858  xrltso  9871  xnn0dcle  9877  xnn0letri  9878  xrpnfdc  9917  xrmnfdc  9918  exfzdc  10316  infssuzex  10323  apbtwnz  10364  expnnval  10634  exp0  10635  bc0k  10848  bcpasc  10858  xrmaxadd  11426  sumdc  11523  zsumdc  11549  fsum3  11552  fisumss  11557  isumss2  11558  fsumsplit  11572  zproddc  11744  fprodseq  11748  fprodssdc  11755  fprodsplitdc  11761  fprodsplit  11762  fprodunsn  11769  fprodcl2lem  11770  fsumdvds  12007  pclemdc  12457  pcxqcl  12481  sumhashdc  12516  1arith  12536  4sqlem17  12576  ctiunctlemudc  12654  lringuplu  13752  suplociccreex  14860  plymullem1  14984  lgsdir2lem5  15273  djurclALT  15448  bj-nn0suc0  15596  trilpolemres  15686  trirec0  15688  nconstwlpolem  15709