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  9702  nn0lt2  9731  zeo  9755  xrltso  10208  xnn0dcle  10214  xnn0letri  10215  apbtwnz  10719  expnegap0  10997  resq01  11108  fzowrddc  11433  xrmaxadd  12043  zsumdc  12167  fsumsplit  12190  sumsplitdc  12215  isumlessdc  12279  zproddc  12362  fprodsplitdc  12379  fprodsplit  12380  fprodunsn  12387  fprodcl2lem  12388  prm23ge5  13063  pcxqcl  13111  gzsum0  13762  lringuplu  14552  aprlring  14649  suplociccreex  15774  lgsdir2lem5  16249  usgredg2v  16563  dichmul0orlem3  16853  dichmul0orlem7  16857  djulclALT  16927  trilpolemres  17189  trirec0  17191  nconstwlpolem0  17211  nconstwlpolem  17213