Theorem orcd 385

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR (\/ insertion right), see natded 23289. (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 378	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  \/wo 361

This theorem is referenced by:  olcd  386  pm2.47  392  orim12i  506  cases2  948  cadan  1427  sbc2or  3172  undif3  3588  rabrsn  3920  disjprg  4263  poxp  6653  unxpwdom2  7750  sornom  8393  fin11a  8499  fin56  8509  fin1a2lem11  8526  axdc3lem2  8567  gchdomtri  8742  0tsk  8868  zmulcl  10638  xrlttri  11061  xmulpnf1  11182  iccsplit  11362  elfznelfzo  11571  ccatsymb  12222  zsum  13136  sumsplit  13176  rpnnen2lem11  13447  sadadd2lem2  13586  vdwlem6  13987  vdwlem10  13991  cshwshashlem1  14062  mreexexlem4d  14525  mreexfidimd  14528  symg2bas  15840  psgnunilem1  15936  gsummulgz  16342  drngnidl  17120  cnsubrg  17583  fctop  18312  cctop  18314  ppttop  18315  pptbas  18316  metusttoOLD  19832  metustto  19833  pmltpclem2  20633  dvne0  21183  taylplem2  21570  taylpfval  21571  dvntaylp0  21578  ang180lem3  21948  scvxcvx  22120  wilthlem2  22148  lgsdir2lem5  22407  tgbtwnconn1  22739  tgbtwnconn2  22740  tgbtwnconn3  22741  legtrid  22754  colinearalglem4  22834  axcontlem3  22891  ex-natded5.7  23297  ex-natded5.13  23301  ex-natded9.20  23303  ex-natded9.20-2  23304  measxun2  26333  measssd  26338  measiun  26341  meascnbl  26342  zprod  27152  sltres  27507  nobnddown  27544  outsideoftr  27862  lineunray  27880  areacirclem4  28158  smprngopr  28523  tsbi1  28615  tsbi2  28616  pell1234qrdich  28875  acongid  28991  acongtr  28994  acongrep  28996  acongeq  28999  jm2.23  29018  jm2.25  29021  jm2.27a  29027  kelac2lem  29090  refsum2cnlem1  29432  wallispilem3  29536  nn0lt2  29860  nn01to3  29861  hashrabsn01  29906  clwlkisclwwlklem2a  30121  frgra2v  30265  frgrawopreg  30316  2spotiundisj  30329  frgrareg  30384  rabsnif  30390  ztprmneprm  30411  gsumXmulgz  30490  lindslinindsimp1  30575  zlmodzxznm  30623  zlmodzxzldeplem4  30629  undif3VD  31196  lkrshpor  32189  2atmat0  32607  dochsnkrlem3  34553

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 179  df-or 363