Theorem orcd 745

Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2 |- ( ph -> ps )
2		orc 724	. 2 |- ( ps -> ( ps \/ ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps \/ ch ) )

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-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  pm2.47  752  orim12i  771  animorl  835  animorrl  838  dcor  948  dfifp2dc  994  undif3ss  3492  dcun  3637  ifeqeqxdc  3687  rabsnifsb  3777  exmidn0m  4338  exmidsssn  4339  reg2exmidlema  4681  acexmidlem1  6081  poxp  6468  nntri2or2  6771  nnm00  6803  ssfilem  7177  ssfilemd  7179  diffitest  7191  tridc  7204  finexdc  7207  elssdc  7209  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  fidcenumlemrks  7270  fdcf1  7316  nninfisollem0  7470  nninfisollemeq  7472  finomni  7480  pr1or2  7540  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem2  7578  netap  7620  2omotaplemap  7623  nqprloc  7912  mullocprlem  7937  recexprlemloc  7998  ltxrlt  8391  zmulcl  9698  nn0lt2  9727  zeo  9751  xrltso  10198  xnn0dcle  10204  xnn0letri  10205  apbtwnz  10709  expnegap0  10984  resq01  11095  fzowrddc  11419  xrmaxadd  12027  zsumdc  12151  fsumsplit  12174  sumsplitdc  12199  isumlessdc  12263  zproddc  12346  fprodsplitdc  12363  fprodsplit  12364  fprodunsn  12371  fprodcl2lem  12372  prm23ge5  13043  pcxqcl  13091  gzsum0  13713  lringuplu  14503  aprlring  14600  suplociccreex  15725  lgsdir2lem5  16151  usgredg2v  16465  dichmul0orlem3  16755  dichmul0orlem7  16759  djulclALT  16829  trilpolemres  17091  trirec0  17093  nconstwlpolem0  17113  nconstwlpolem  17115