Theorem orcd 392

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR (\/ insertion right), see natded 24079. (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  963  cadan  1434  sbc2or  3306  undif3  3725  rabsnifsb  4060  disjprg  4405  poxp  6818  unxpwdom2  7940  sornom  8583  fin11a  8689  fin56  8699  fin1a2lem11  8716  axdc3lem2  8757  gchdomtri  8933  0tsk  9059  zmulcl  10831  xrlttri  11255  xmulpnf1  11376  iccsplit  11563  elfznelfzo  11775  ccatsymb  12439  zsum  13353  sumsplit  13393  rpnnen2lem11  13665  sadadd2lem2  13804  vdwlem6  14205  vdwlem10  14209  cshwshashlem1  14280  mreexexlem4d  14744  mreexfidimd  14747  symg2bas  16062  psgnunilem1  16158  gsummulgz  16601  srgbinomlem4  16817  drngnidl  17487  cnsubrg  18066  fctop  19007  cctop  19009  ppttop  19010  pptbas  19011  metusttoOLD  20531  metustto  20532  pmltpclem2  21332  dvne0  21883  taylplem2  22229  taylpfval  22230  dvntaylp0  22237  ang180lem3  22607  scvxcvx  22779  wilthlem2  22807  lgsdir2lem5  23066  tgbtwnconn1  23425  tgbtwnconn2  23426  tgbtwnconn3  23427  legtrid  23441  ncolne1  23455  tglineneq  23473  ncolncol  23475  coltr2  23477  colmid  23509  footex  23539  colperpexlem3  23547  colperpex  23548  mideulem  23549  hypcgrlem1  23577  hypcgrlem2  23578  colinearalglem4  23624  axcontlem3  23681  ex-natded5.7  24087  ex-natded5.13  24091  ex-natded9.20  24093  ex-natded9.20-2  24094  measxun2  27081  measssd  27086  measiun  27089  meascnbl  27090  zprod  27906  sltres  28261  nobnddown  28298  outsideoftr  28616  lineunray  28634  areacirclem4  28947  smprngopr  29312  tsbi1  29404  tsbi2  29405  pell1234qrdich  29662  acongid  29778  acongtr  29781  acongrep  29783  acongeq  29786  jm2.23  29805  jm2.25  29808  jm2.27a  29814  kelac2lem  29877  refsum2cnlem1  30219  limciccioolb  30392  limcicciooub  30408  cncfiooicclem1  30461  wallispilem3  30596  fourierdlem35  30671  fourierdlem80  30716  fouriersw  30761  nn0lt2  31063  nn01to3  31064  hashrabsn01  31109  clwlkisclwwlklem2a  31324  frgra2v  31468  frgrawopreg  31519  2spotiundisj  31532  frgrareg  31587  ztprmneprm  31613  altgsumbcALT  31619  lindslinindsimp1  31763  zlmodzxznm  31811  zlmodzxzldeplem4  31817  chfacfscmulgsum  31858  chfacfpmmulgsum  31862  undif3VD  32461  bj-animorl  32916  bj-animorrl  32919  lkrshpor  33603  2atmat0  34021  dochsnkrlem3  35967

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