Theorem orcd 738

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 717	. 2 |- ( ps -> ( ps \/ ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps \/ ch ) )

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  739  pm2.47  745  orim12i  764  animorl  828  animorrl  831  dcor  941  dfifp2dc  987  undif3ss  3465  dcun  3601  exmidn0m  4285  exmidsssn  4286  reg2exmidlema  4626  acexmidlem1  6003  poxp  6384  nntri2or2  6652  nnm00  6684  ssfilem  7045  diffitest  7057  tridc  7070  finexdc  7073  elssdc  7075  fientri3  7088  unsnfidcex  7093  unsnfidcel  7094  fidcenumlemrks  7131  nninfisollem0  7308  nninfisollemeq  7310  finomni  7318  pr1or2  7378  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  exmidontriimlem2  7415  netap  7451  2omotaplemap  7454  nqprloc  7743  mullocprlem  7768  recexprlemloc  7829  ltxrlt  8223  zmulcl  9511  nn0lt2  9539  zeo  9563  xrltso  10004  xnn0dcle  10010  xnn0letri  10011  apbtwnz  10506  expnegap0  10781  fzowrddc  11195  xrmaxadd  11788  zsumdc  11911  fsumsplit  11934  sumsplitdc  11959  isumlessdc  12023  zproddc  12106  fprodsplitdc  12123  fprodsplit  12124  fprodunsn  12131  fprodcl2lem  12132  prm23ge5  12803  pcxqcl  12851  gsum0g  13445  lringuplu  14176  suplociccreex  15314  lgsdir2lem5  15727  usgredg2v  16038  djulclALT  16248  trilpolemres  16498  trirec0  16500  nconstwlpolem0  16519  nconstwlpolem  16521