Theorem orcd 407

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

Syntax hints:   -> wi 4   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  olcd  408  pm2.47  414  animorl  505  animorrl  508  orim12i  538  cases2  993  sbc2or  3444  undif3OLD  3889  rabsnifsb  4257  n0snor2el  4364  disjprg  4648  propeqop  4970  poxp  7289  unxpwdom2  8493  sornom  9099  fin11a  9205  fin56  9215  fin1a2lem11  9232  axdc3lem2  9273  gchdomtri  9451  0tsk  9577  zmulcl  11426  nn0lt2  11440  nn01to3  11781  xrlttri  11972  xmulpnf1  12104  iccsplit  12305  elfznelfzo  12573  hashrabsn01  13162  hashsn01  13204  ccatsymb  13366  zsum  14449  sumsplit  14499  zprod  14667  rpnnen2lem11  14953  sadadd2lem2  15172  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  vdwlem6  15690  vdwlem10  15694  cshwshashlem1  15802  basprssdmsets  15925  mreexexlem4d  16307  mreexfidimd  16311  sgrp2nmndlem5  17416  symg2bas  17818  psgnunilem1  17913  gsummulgz  18343  srgbinomlem4  18543  drngnidl  19229  cnsubrg  19806  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  fctop  20808  cctop  20810  ppttop  20811  pptbas  20812  metustto  22358  pmltpclem2  23218  dvne0  23774  taylplem2  24118  taylpfval  24119  dvntaylp0  24126  ang180lem3  24541  scvxcvx  24712  wilthlem2  24795  lgsdir2lem5  25054  tgbtwnconn1  25470  tgbtwnconn2  25471  tgbtwnconn3  25472  legtrid  25486  hltr  25505  hlbtwn  25506  btwnhl1  25507  btwnhl2  25508  tglineneq  25539  ncolncol  25541  colmid  25583  footex  25613  colperpexlem3  25624  colperpex  25625  mideulem2  25626  opphllem  25627  hlpasch  25648  colhp  25662  hphl  25663  hypcgrlem1  25691  hypcgrlem2  25692  trgcopy  25696  trgcopyeulem  25697  cgracgr  25710  cgraswap  25712  cgrahl  25718  cgracol  25719  inaghl  25731  colinearalglem4  25789  axcontlem3  25846  edglnl  26038  clwlkclwwlklem2a  26899  trlsegvdeg  27087  nfrgr2v  27136  frgrwopreg  27187  frgrreg  27252  ex-natded5.7  27268  ex-natded5.13  27272  ex-natded9.20  27274  ex-natded9.20-2  27275  padct  29497  f1ocnt  29559  submateqlem2  29874  measxun2  30273  measssd  30278  measiun  30281  meascnbl  30282  carsgclctun  30383  sltres  31815  outsideoftr  32236  lineunray  32254  knoppndvlem6  32508  topdifinffinlem  33195  areacirclem4  33503  smprngopr  33851  tsbi1  33940  tsbi2  33941  lkrshpor  34394  2atmat0  34812  dochsnkrlem3  36760  pell1234qrdich  37425  acongid  37542  acongtr  37545  acongrep  37547  acongeq  37550  jm2.23  37563  jm2.25  37566  jm2.27a  37572  kelac2lem  37634  rp-fakeimass  37857  frege106d  38047  clsk1indlem3  38341  nanorxor  38504  undif3VD  39118  refsum2cnlem1  39196  reclt0d  39607  limciccioolb  39853  limcicciooub  39869  wallispilem3  40284  fourierdlem35  40359  fourierdlem80  40403  fourierswlem  40447  fouriersw  40448  nltle2tri  41323  icceuelpartlem  41371  even3prm2  41628  stgoldbwt  41664  nrhmzr  41873  ztprmneprm  42125  altgsumbcALT  42131  lindslinindsimp1  42246  zlmodzxznm  42286  zlmodzxzldeplem4  42292