Theorem orcd 399

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

Syntax hints:   -> wi 4   \/ wo 375

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 190  df-or 377

This theorem is referenced by:  olcd  400  pm2.47  406  orim12i  525  cases2  982  cadan  1520  sbc2or  3264  undif3  3695  rabsnifsb  4031  disjprg  4391  poxp  6927  unxpwdom2  8121  sornom  8725  fin11a  8831  fin56  8841  fin1a2lem11  8858  axdc3lem2  8899  gchdomtri  9072  0tsk  9198  zmulcl  11009  nn0lt2  11023  nn01to3  11280  xrlttri  11461  xmulpnf1  11585  iccsplit  11791  elfznelfzo  12045  hashrabsn01  12590  hashsn01  12631  ccatsymb  12778  zsum  13861  sumsplit  13906  zprod  14068  rpnnen2lem11  14354  sadadd2lem2  14503  lcmfunsnlem2lem1  14690  lcmfunsnlem2  14692  vdwlem6  15015  vdwlem10  15019  cshwshashlem1  15144  mreexexlem4d  15631  mreexfidimd  15634  sgrp2nmndlem5  16741  symg2bas  17117  psgnunilem1  17212  gsummulgz  17654  srgbinomlem4  17854  drngnidl  18530  cnsubrg  19105  chfacfscmulgsum  19961  chfacfpmmulgsum  19965  fctop  20096  cctop  20098  ppttop  20099  pptbas  20100  metustto  21646  pmltpclem2  22478  dvne0  23042  taylplem2  23398  taylpfval  23399  dvntaylp0  23406  ang180lem3  23819  scvxcvx  23990  wilthlem2  24073  lgsdir2lem5  24334  tgbtwnconn1  24699  tgbtwnconn2  24700  tgbtwnconn3  24701  legtrid  24715  hltr  24734  hlbtwn  24735  btwnhl1  24736  btwnhl2  24737  tglineneq  24768  ncolncol  24770  colmid  24812  footex  24842  colperpexlem3  24853  colperpex  24854  mideulem2  24855  opphllem  24856  hlpasch  24877  colhp  24891  hphl  24892  hypcgrlem1  24920  hypcgrlem2  24921  trgcopy  24925  trgcopyeulem  24926  cgracgr  24939  cgraswap  24941  cgrahl  24947  cgracol  24948  inaghl  24960  colinearalglem4  25018  axcontlem3  25075  clwlkisclwwlklem2a  25592  frgra2v  25806  frgrawopreg  25856  2spotiundisj  25869  frgrareg  25924  ex-natded5.7  25940  ex-natded5.13  25944  ex-natded9.20  25946  ex-natded9.20-2  25947  padct  28382  f1ocnt  28451  submateqlem2  28708  measxun2  29106  measssd  29111  measiun  29114  meascnbl  29115  carsgclctun  29226  sltres  30622  nobnddown  30661  outsideoftr  30967  lineunray  30985  bj-animorl  31212  bj-animorrl  31215  topdifinffinlem  31820  areacirclem4  32099  smprngopr  32349  tsbi1  32439  tsbi2  32440  lkrshpor  32744  2atmat0  33162  dochsnkrlem3  35110  pell1234qrdich  35778  acongid  35896  acongtr  35899  acongrep  35901  acongeq  35904  jm2.23  35922  jm2.25  35925  jm2.27a  35931  kelac2lem  35993  rp-fakeimass  36227  frege106d  36418  nanorxor  36723  undif3VD  37342  refsum2cnlem1  37421  limciccioolb  37798  limcicciooub  37814  wallispilem3  38041  fourierdlem35  38117  fourierdlem80  38162  fourierswlem  38206  fouriersw  38207  nltle2tri  38861  icceuelpartlem  38894  stgoldbwt  39022  n0snor2el  39143  propeqop  39146  trlsegvdeg  40139  nrhmzr  40381  ztprmneprm  40636  altgsumbcALT  40642  lindslinindsimp1  40758  zlmodzxznm  40798  zlmodzxzldeplem4  40804