Theorem orcd 392

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR ( \/ insertion right), see natded 25102. (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  971  cases2OLD  972  cadan  1447  sbc2or  3322  undif3  3744  rabsnifsb  4083  disjprg  4433  poxp  6897  unxpwdom2  8017  sornom  8660  fin11a  8766  fin56  8776  fin1a2lem11  8793  axdc3lem2  8834  gchdomtri  9010  0tsk  9136  zmulcl  10919  nn0lt2  10934  nn01to3  11186  xrlttri  11356  xmulpnf1  11477  iccsplit  11664  elfznelfzo  11897  hashrabsn01  12423  ccatsymb  12582  ccat2s1fvw  12624  zsum  13522  sumsplit  13565  zprod  13726  rpnnen2lem11  13940  sadadd2lem2  14082  vdwlem6  14486  vdwlem10  14490  cshwshashlem1  14562  mreexexlem4d  15026  mreexfidimd  15029  sgrp2nmndlem5  16026  symg2bas  16402  psgnunilem1  16497  gsummulgz  16945  srgbinomlem4  17173  drngnidl  17856  cnsubrg  18457  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  fctop  19483  cctop  19485  ppttop  19486  pptbas  19487  metusttoOLD  21038  metustto  21039  pmltpclem2  21839  dvne0  22390  taylplem2  22737  taylpfval  22738  dvntaylp0  22745  ang180lem3  23121  scvxcvx  23293  wilthlem2  23321  lgsdir2lem5  23580  tgbtwnconn1  23940  tgbtwnconn2  23941  tgbtwnconn3  23942  legtrid  23956  hltr  23972  hlbtwn  23973  btwnhl1  23974  btwnhl2  23975  tglineneq  24002  ncolncol  24004  coltr2  24006  colmid  24043  footex  24073  colperpexlem3  24084  colperpex  24085  mideulem2  24086  opphllem  24087  hypcgrlem1  24142  hypcgrlem2  24143  colinearalglem4  24190  axcontlem3  24247  clwlkisclwwlklem2a  24763  frgra2v  24977  frgrawopreg  25027  2spotiundisj  25040  frgrareg  25095  ex-natded5.7  25110  ex-natded5.13  25114  ex-natded9.20  25116  ex-natded9.20-2  25117  measxun2  28159  measssd  28164  measiun  28167  meascnbl  28168  sltres  29400  nobnddown  29437  outsideoftr  29755  lineunray  29773  areacirclem4  30086  smprngopr  30425  tsbi1  30516  tsbi2  30517  pell1234qrdich  30773  acongid  30889  acongtr  30892  acongrep  30894  acongeq  30897  jm2.23  30914  jm2.25  30917  jm2.27a  30923  kelac2lem  30986  nanorxor  31161  refsum2cnlem1  31366  limciccioolb  31581  limcicciooub  31597  wallispilem3  31803  fourierdlem35  31878  fourierdlem80  31923  fourierswlem  31967  fouriersw  31968  ztprmneprm  32804  altgsumbcALT  32810  lindslinindsimp1  32928  zlmodzxznm  32968  zlmodzxzldeplem4  32974  undif3VD  33550  bj-animorl  34018  bj-animorrl  34021  lkrshpor  34707  2atmat0  35125  dochsnkrlem3  37073  rp-fakeimass  37574