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 ) )

Syntax hints:   -> wi 4   \/ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  753  pm2.49  754  orim12i  771  pm1.5  777  animorr  836  animorlr  837  dcor  948  dfifp2dc  994  dcfrompeirce  1499  dcun  3634  exmidn0m  4333  regexmidlem1  4675  reg2exmidlema  4676  nn0suc  4746  nndceq0  4760  acexmidlem1  6071  nntri3or  6756  nntri2or2  6761  nndceq  6762  nndcel  6763  nnm00  6793  ssfilem  7167  ssfilemd  7169  diffitest  7181  tridc  7194  finexdc  7197  elssdc  7199  eqsndc  7200  fientri3  7212  unsnfidcex  7217  unsnfidcel  7218  fidcenumlemrks  7260  fidcenumlemrk  7261  nninfisollemne  7461  nninfisol  7463  finomni  7470  pr1or2  7530  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  exmidontriimlem2  7568  netap  7610  2omotaplemap  7613  mullocprlem  7927  recexprlemloc  7988  gt0ap0  8944  ltap  8951  recexaplem2  8970  nn1m1nn  9301  nn1gt1  9317  ltpnf  10161  mnflt  10164  xrltso  10177  xnn0dcle  10183  xnn0letri  10184  xrpnfdc  10223  xrmnfdc  10224  exfzdc  10637  infssuzex  10644  apbtwnz  10687  expnnval  10957  exp0  10958  resq01  11073  bc0k  11172  bcpasc  11182  ccatsymb  11348  xrmaxadd  12005  sumdc  12102  zsumdc  12129  fsum3  12132  fisumss  12137  isumss2  12138  fsumsplit  12152  zproddc  12324  fprodseq  12328  fprodssdc  12335  fprodsplitdc  12341  fprodsplit  12342  fprodunsn  12349  fprodcl2lem  12350  fsumdvds  12587  pclemdc  13045  pcxqcl  13069  sumhashdc  13104  1arith  13124  4sqlem17  13164  ctiunctlemudc  13306  lringuplu  14476  aprlring  14573  suplociccreex  15648  plymullem1  15772  lgsdir2lem5  16065  upgr1een  16279  umgrvad2edg  16366  usgr1e  16396  eupth2lem2dc  16614  eupth2lem3lem4fi  16628  dichmul0orlem3  16669  dichmul0orlem7  16673  djurclALT  16744  bj-nn0suc0  16890  trilpolemres  16996  trirec0  16998  nconstwlpolem  17020