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  4338  regexmidlem1  4680  reg2exmidlema  4681  nn0suc  4751  nndceq0  4765  acexmidlem1  6081  nntri3or  6766  nntri2or2  6771  nndceq  6772  nndcel  6773  nnm00  6803  ssfilem  7177  ssfilemd  7179  diffitest  7191  tridc  7204  finexdc  7207  elssdc  7209  eqsndc  7210  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  fidcenumlemrks  7270  fidcenumlemrk  7271  nninfisollemne  7471  nninfisol  7473  finomni  7480  pr1or2  7540  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem2  7578  netap  7620  2omotaplemap  7623  mullocprlem  7937  recexprlemloc  7998  gt0ap0  8956  ltap  8963  recexaplem2  8982  nn1m1nn  9324  nn1gt1  9340  ltpnf  10192  mnflt  10195  xrltso  10208  xnn0dcle  10214  xnn0letri  10215  xrpnfdc  10254  xrmnfdc  10255  exfzdc  10669  infssuzex  10676  apbtwnz  10719  expnnval  10992  exp0  10993  resq01  11108  bc0k  11208  bcpasc  11218  ccatsymb  11384  xrmaxadd  12043  sumdc  12140  zsumdc  12167  fsum3  12170  fisumss  12175  isumss2  12176  fsumsplit  12190  zproddc  12362  fprodseq  12366  fprodssdc  12373  fprodsplitdc  12379  fprodsplit  12380  fprodunsn  12387  fprodcl2lem  12388  fsumdvds  12625  prmdcz  12925  pclemdc  13087  pcxqcl  13111  sumhashdc  13146  1arith  13166  4sqlem17  13206  ctiunctlemudc  13377  lringuplu  14552  aprlring  14649  suplociccreex  15774  plymullem1  15898  lgsdir2lem5  16249  upgr1een  16463  umgrvad2edg  16550  usgr1e  16580  eupth2lem2dc  16798  eupth2lem3lem4fi  16812  dichmul0orlem3  16853  dichmul0orlem7  16857  djurclALT  16928  bj-nn0suc0  17074  trilpolemres  17189  trirec0  17191  nconstwlpolem  17213