Theorem orcd 392

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR (\/ insertion right), see natded 25124. (Contributed by NM, 20-Sep-2007.)

Hypothesis

Ref	Expression
orcd.1

Assertion

Ref	Expression
orcd

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2
2		orc 385	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  \/wo 368

This theorem is referenced by:  olcd  393  pm2.47  399  orim12i  516  cases2  971  cadan  1459  sbc2or  3336  undif3  3758  rabsnifsb  4098  disjprg  4448  poxp  6912  unxpwdom2  8035  sornom  8678  fin11a  8784  fin56  8794  fin1a2lem11  8811  axdc3lem2  8852  gchdomtri  9028  0tsk  9154  zmulcl  10937  nn0lt2  10952  nn01to3  11204  xrlttri  11374  xmulpnf1  11495  iccsplit  11682  elfznelfzo  11915  hashrabsn01  12441  ccatsymb  12600  ccat2s1fvw  12642  zsum  13540  sumsplit  13583  zprod  13744  rpnnen2lem11  13958  sadadd2lem2  14100  vdwlem6  14504  vdwlem10  14508  cshwshashlem1  14580  mreexexlem4d  15044  mreexfidimd  15047  sgrp2nmndlem5  16047  symg2bas  16423  psgnunilem1  16518  gsummulgz  16966  srgbinomlem4  17194  drngnidl  17877  cnsubrg  18478  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  fctop  19505  cctop  19507  ppttop  19508  pptbas  19509  metusttoOLD  21060  metustto  21061  pmltpclem2  21861  dvne0  22412  taylplem2  22759  taylpfval  22760  dvntaylp0  22767  ang180lem3  23143  scvxcvx  23315  wilthlem2  23343  lgsdir2lem5  23602  tgbtwnconn1  23962  tgbtwnconn2  23963  tgbtwnconn3  23964  legtrid  23978  hltr  23994  hlbtwn  23995  btwnhl1  23996  btwnhl2  23997  tglineneq  24024  ncolncol  24026  coltr2  24028  colmid  24065  footex  24095  colperpexlem3  24106  colperpex  24107  mideulem2  24108  opphllem  24109  hypcgrlem1  24164  hypcgrlem2  24165  colinearalglem4  24212  axcontlem3  24269  clwlkisclwwlklem2a  24785  frgra2v  24999  frgrawopreg  25049  2spotiundisj  25062  frgrareg  25117  ex-natded5.7  25132  ex-natded5.13  25136  ex-natded9.20  25138  ex-natded9.20-2  25139  measxun2  28181  measssd  28186  measiun  28189  meascnbl  28190  sltres  29424  nobnddown  29461  outsideoftr  29779  lineunray  29797  areacirclem4  30110  smprngopr  30449  tsbi1  30540  tsbi2  30541  pell1234qrdich  30797  acongid  30913  acongtr  30916  acongrep  30918  acongeq  30921  jm2.23  30938  jm2.25  30941  jm2.27a  30947  kelac2lem  31010  nanorxor  31185  refsum2cnlem1  31412  limciccioolb  31627  limcicciooub  31643  wallispilem3  31849  fourierdlem35  31924  fourierdlem80  31969  fourierswlem  32013  fouriersw  32014  nrhmzr  32679  ztprmneprm  32936  altgsumbcALT  32942  lindslinindsimp1  33058  zlmodzxznm  33098  zlmodzxzldeplem4  33104  undif3VD  33682  bj-animorl  34150  bj-animorrl  34153  lkrshpor  34832  2atmat0  35250  dochsnkrlem3  37198  rp-fakeimass  37736

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