Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  orcd Unicode version

Theorem orcd 723
 Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
Hypothesis
Ref Expression
orcd.1
Assertion
Ref Expression
orcd

Proof of Theorem orcd
StepHypRef Expression
1 orcd.1 . 2
2 orc 702 . 2
31, 2syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  olcd  724  pm2.47  730  orim12i  749  dcor  920  undif3ss  3368  dcun  3504  exmidn0m  4161  exmidsssn  4162  reg2exmidlema  4491  acexmidlem1  5814  poxp  6173  nntri2or2  6438  nnm00  6469  ssfilem  6813  diffitest  6825  tridc  6837  finexdc  6840  fientri3  6852  unsnfidcex  6857  unsnfidcel  6858  fidcenumlemrks  6890  finomni  7066  exmidfodomrlemeldju  7117  exmidfodomrlemreseldju  7118  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  exmidaclem  7126  exmidontriimlem2  7140  nqprloc  7448  mullocprlem  7473  recexprlemloc  7534  ltxrlt  7926  zmulcl  9203  nn0lt2  9228  zeo  9252  xrltso  9685  apbtwnz  10155  expnegap0  10409  xrmaxadd  11140  zsumdc  11263  fsumsplit  11286  sumsplitdc  11311  isumlessdc  11375  zproddc  11458  fprodsplitdc  11475  fprodsplit  11476  fprodunsn  11483  fprodcl2lem  11484  suplociccreex  12962  djulclALT  13335  trilpolemres  13576  trirec0  13578  nconstwlpolem0  13596  nconstwlpolem  13598
 Copyright terms: Public domain W3C validator