Theorem olcd 739

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  746  pm2.49  747  orim12i  764  pm1.5  770  animorr  829  animorlr  830  dcor  941  dfifp2dc  987  dcfrompeirce  1492  dcun  3601  exmidn0m  4285  regexmidlem1  4625  reg2exmidlema  4626  nn0suc  4696  nndceq0  4710  acexmidlem1  6003  nntri3or  6647  nntri2or2  6652  nndceq  6653  nndcel  6654  nnm00  6684  ssfilem  7045  diffitest  7057  tridc  7070  finexdc  7073  elssdc  7075  eqsndc  7076  fientri3  7088  unsnfidcex  7093  unsnfidcel  7094  fidcenumlemrks  7131  fidcenumlemrk  7132  nninfisollemne  7309  nninfisol  7311  finomni  7318  pr1or2  7378  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  exmidontriimlem2  7415  netap  7451  2omotaplemap  7454  mullocprlem  7768  recexprlemloc  7829  gt0ap0  8784  ltap  8791  recexaplem2  8810  nn1m1nn  9139  nn1gt1  9155  ltpnf  9988  mnflt  9991  xrltso  10004  xnn0dcle  10010  xnn0letri  10011  xrpnfdc  10050  xrmnfdc  10051  exfzdc  10458  infssuzex  10465  apbtwnz  10506  expnnval  10776  exp0  10777  bc0k  10990  bcpasc  11000  ccatsymb  11150  xrmaxadd  11788  sumdc  11885  zsumdc  11911  fsum3  11914  fisumss  11919  isumss2  11920  fsumsplit  11934  zproddc  12106  fprodseq  12110  fprodssdc  12117  fprodsplitdc  12123  fprodsplit  12124  fprodunsn  12131  fprodcl2lem  12132  fsumdvds  12369  pclemdc  12827  pcxqcl  12851  sumhashdc  12886  1arith  12906  4sqlem17  12946  ctiunctlemudc  13024  lringuplu  14176  suplociccreex  15314  plymullem1  15438  lgsdir2lem5  15727  umgrvad2edg  16025  djurclALT  16249  bj-nn0suc0  16396  trilpolemres  16498  trirec0  16500  nconstwlpolem  16521