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  7471  nninfisollemeq  7473  finomni  7481  pr1or2  7541  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  exmidontriimlem2  7579  netap  7621  2omotaplemap  7624  nqprloc  7913  mullocprlem  7938  recexprlemloc  7999  ltxrlt  8392  zmulcl  9703  nn0lt2  9732  zeo  9756  xrltso  10209  xnn0dcle  10215  xnn0letri  10216  apbtwnz  10720  expnegap0  10999  resq01  11110  fzowrddc  11435  xrmaxadd  12046  zsumdc  12170  fsumsplit  12193  sumsplitdc  12218  isumlessdc  12282  zproddc  12365  fprodsplitdc  12382  fprodsplit  12383  fprodunsn  12390  fprodcl2lem  12391  prm23ge5  13066  pcxqcl  13114  gzsum0  13766  lringuplu  14587  aprlring  14684  suplociccreex  15816  lgsdir2lem5  16317  usgredg2v  16631  dichmul0orlem3  16921  dichmul0orlem7  16925  djulclALT  16995  trilpolemres  17258  trirec0  17260  nconstwlpolem0  17280  nconstwlpolem  17282