Theorem orcd 741

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

Syntax hints:   -> wi 4   \/ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  742  pm2.47  748  orim12i  767  animorl  831  animorrl  834  dcor  944  dfifp2dc  990  undif3ss  3482  dcun  3619  rabsnifsb  3757  exmidn0m  4314  exmidsssn  4315  reg2exmidlema  4656  acexmidlem1  6046  poxp  6428  nntri2or2  6731  nnm00  6763  ssfilem  7130  ssfilemd  7132  diffitest  7144  tridc  7157  finexdc  7160  elssdc  7162  fientri3  7175  unsnfidcex  7180  unsnfidcel  7181  fidcenumlemrks  7223  nninfisollem0  7421  nninfisollemeq  7423  finomni  7431  pr1or2  7491  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  exmidontriimlem2  7529  netap  7568  2omotaplemap  7571  nqprloc  7860  mullocprlem  7885  recexprlemloc  7946  ltxrlt  8339  zmulcl  9631  nn0lt2  9659  zeo  9683  xrltso  10129  xnn0dcle  10135  xnn0letri  10136  apbtwnz  10634  expnegap0  10909  fzowrddc  11339  xrmaxadd  11946  zsumdc  12070  fsumsplit  12093  sumsplitdc  12118  isumlessdc  12182  zproddc  12265  fprodsplitdc  12282  fprodsplit  12283  fprodunsn  12290  fprodcl2lem  12291  prm23ge5  12962  pcxqcl  13010  gsum0g  13609  lringuplu  14341  aprlring  14434  suplociccreex  15489  lgsdir2lem5  15905  usgredg2v  16219  djulclALT  16573  trilpolemres  16826  trirec0  16828  trimul0or  16845  nconstwlpolem0  16849  nconstwlpolem  16851