Theorem orcd 382

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR ( \/ insertion right), see natded 21664. (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 375	. 2 |- ( ps -> ( ps \/ ch ) )
3	1, 2	syl 16	1 |- ( ph -> ( ps \/ ch ) )

Syntax hints:   -> wi 4   \/ wo 358

This theorem is referenced by:  olcd  383  pm2.47  389  orim12i  503  sbc2or  3129  undif3  3562  rabrsn  3834  disjprg  4168  poxp  6417  unxpwdom2  7512  sornom  8113  fin11a  8219  fin56  8229  fin1a2lem11  8246  axdc3lem2  8287  gchdomtri  8460  0tsk  8586  zmulcl  10280  xrlttri  10688  xmulpnf1  10809  iccsplit  10985  elfznelfzo  11147  zsum  12467  sumsplit  12507  rpnnen2lem11  12779  sadadd2lem2  12917  vdwlem6  13309  vdwlem10  13313  mreexexlem4d  13827  mreexfidimd  13830  gsummulgz  15493  drngnidl  16255  cnsubrg  16714  fctop  17023  cctop  17025  ppttop  17026  pptbas  17027  metusttoOLD  18540  metustto  18541  pmltpclem2  19299  dvne0  19848  taylplem2  20233  taylpfval  20234  dvntaylp0  20241  ang180lem3  20606  scvxcvx  20777  wilthlem2  20805  lgsdir2lem5  21064  ex-natded5.7  21672  ex-natded5.13  21676  ex-natded9.20  21678  ex-natded9.20-2  21679  measxun2  24517  measssd  24522  measiun  24525  meascnbl  24526  sibfof  24607  zprod  25216  sltres  25532  nobnddown  25569  colinearalglem4  25752  axcontlem3  25809  outsideoftr  25967  lineunray  25985  areacirclem5  26185  smprngopr  26552  pell1234qrdich  26814  acongid  26930  acongtr  26933  acongrep  26935  acongeq  26938  jm2.23  26957  jm2.25  26960  jm2.27a  26966  kelac2lem  27030  psgnunilem1  27284  refsum2cnlem1  27575  wallispilem3  27683  frgrawopreg  28152  2spotiundisj  28165  undif3VD  28703  lkrshpor  29590  2atmat0  30008  dochsnkrlem3  31954

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-or 360