Theorem orcd 392

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

Syntax hints:   -> wi 4   \/ wo 368

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

This theorem depends on definitions:  df-bi 185  df-or 370

This theorem is referenced by:  olcd  393  pm2.47  399  orim12i  516  cases2  970  cases2OLD  971  cadan  1443  sbc2or  3340  undif3  3759  rabsnifsb  4095  disjprg  4443  poxp  6892  unxpwdom2  8010  sornom  8653  fin11a  8759  fin56  8769  fin1a2lem11  8786  axdc3lem2  8827  gchdomtri  9003  0tsk  9129  zmulcl  10907  nn0lt2  10921  nn01to3  11171  xrlttri  11341  xmulpnf1  11462  iccsplit  11649  elfznelfzo  11879  hashrabsn01  12405  ccatsymb  12561  ccat2s1fvw  12601  zsum  13499  sumsplit  13542  rpnnen2lem11  13815  sadadd2lem2  13955  vdwlem6  14359  vdwlem10  14363  cshwshashlem1  14434  mreexexlem4d  14898  mreexfidimd  14901  symg2bas  16218  psgnunilem1  16314  gsummulgz  16757  srgbinomlem4  16982  drngnidl  17659  cnsubrg  18246  chfacfscmulgsum  19128  chfacfpmmulgsum  19132  fctop  19271  cctop  19273  ppttop  19274  pptbas  19275  metusttoOLD  20795  metustto  20796  pmltpclem2  21596  dvne0  22147  taylplem2  22493  taylpfval  22494  dvntaylp0  22501  ang180lem3  22871  scvxcvx  23043  wilthlem2  23071  lgsdir2lem5  23330  tgbtwnconn1  23689  tgbtwnconn2  23690  tgbtwnconn3  23691  legtrid  23705  ncolne1  23719  tglineneq  23737  ncolncol  23739  coltr2  23741  colmid  23773  footex  23803  colperpexlem3  23811  colperpex  23812  mideulem  23813  hypcgrlem1  23841  hypcgrlem2  23842  colinearalglem4  23888  axcontlem3  23945  clwlkisclwwlklem2a  24461  frgra2v  24675  frgrawopreg  24726  2spotiundisj  24739  frgrareg  24794  ex-natded5.7  24809  ex-natded5.13  24813  ex-natded9.20  24815  ex-natded9.20-2  24816  measxun2  27821  measssd  27826  measiun  27829  meascnbl  27830  zprod  28646  sltres  29001  nobnddown  29038  outsideoftr  29356  lineunray  29374  areacirclem4  29687  smprngopr  30052  tsbi1  30144  tsbi2  30145  pell1234qrdich  30401  acongid  30517  acongtr  30520  acongrep  30522  acongeq  30525  jm2.23  30542  jm2.25  30545  jm2.27a  30551  kelac2lem  30614  refsum2cnlem1  30990  limciccioolb  31163  limcicciooub  31179  cncfiooicclem1  31232  wallispilem3  31367  fourierdlem35  31442  fourierdlem80  31487  fouriersw  31532  ztprmneprm  32000  altgsumbcALT  32006  lindslinindsimp1  32131  zlmodzxznm  32179  zlmodzxzldeplem4  32185  undif3VD  32762  bj-animorl  33217  bj-animorrl  33220  lkrshpor  33904  2atmat0  34322  dochsnkrlem3  36268