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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  746  pm2.47  752  orim12i  771  animorl  835  animorrl  838  dcor  948  dfifp2dc  994  undif3ss  3492  dcun  3634  ifeqeqxdc  3684  rabsnifsb  3773  exmidn0m  4333  exmidsssn  4334  reg2exmidlema  4676  acexmidlem1  6071  poxp  6458  nntri2or2  6761  nnm00  6793  ssfilem  7167  ssfilemd  7169  diffitest  7181  tridc  7194  finexdc  7197  elssdc  7199  fientri3  7212  unsnfidcex  7217  unsnfidcel  7218  fidcenumlemrks  7260  fdcf1  7306  nninfisollem0  7460  nninfisollemeq  7462  finomni  7470  pr1or2  7530  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  exmidontriimlem2  7568  netap  7610  2omotaplemap  7613  nqprloc  7902  mullocprlem  7927  recexprlemloc  7988  ltxrlt  8381  zmulcl  9677  nn0lt2  9706  zeo  9730  xrltso  10177  xnn0dcle  10183  xnn0letri  10184  apbtwnz  10687  expnegap0  10962  resq01  11073  fzowrddc  11397  xrmaxadd  12005  zsumdc  12129  fsumsplit  12152  sumsplitdc  12177  isumlessdc  12241  zproddc  12324  fprodsplitdc  12341  fprodsplit  12342  fprodunsn  12349  fprodcl2lem  12350  prm23ge5  13021  pcxqcl  13069  gzsum0  13690  lringuplu  14476  aprlring  14573  suplociccreex  15648  lgsdir2lem5  16065  usgredg2v  16379  dichmul0orlem3  16669  dichmul0orlem7  16673  djulclALT  16743  trilpolemres  16996  trirec0  16998  nconstwlpolem0  17018  nconstwlpolem  17020