MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  olcd Unicode version

Theorem olcd 393
Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IL (\/ insertion left), see natded 25124. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
Hypothesis
Ref Expression
orcd.1
Assertion
Ref Expression
olcd

Proof of Theorem olcd
StepHypRef Expression
1 orcd.1 . . 3
21orcd 392 . 2
32orcomd 388 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368
This theorem is referenced by:  pm2.48  400  pm2.49  401  orim12i  516  pm1.5  522  cases2  971  otsndisj  4757  otiunsndisj  4758  somin1  5408  soxp  6913  fowdom  8018  unxpwdom2  8035  fin1a2lem11  8811  axdc3lem2  8852  gchdomtri  9028  hargch  9072  alephgch  9073  nn1m1nn  10581  nn01to3  11204  rpneg  11278  ltpnf  11360  mnflt  11362  xrlttri  11374  xmulpnf1  11495  iccsplit  11682  elfznelfzo  11915  bc0k  12389  bcpasc  12399  hashv01gt1  12418  hashrabsn01  12441  hashf1  12506  pr2pwpr  12520  hashtpg  12523  ffz0iswrd  12568  wrdsymb0  12575  ccatsymb  12600  fsum  13542  fsumsplit  13562  fprod  13748  fsumdvds  14029  sumhash  14415  4sqlem17  14479  vdwlem6  14504  ram0  14540  cshwsidrepswmod0  14579  cshwsdisj  14583  mreexfidimd  15047  sgrp2nmndlem5  16047  psgnunilem1  16518  psgnunilem5  16519  gsummulg  16965  srgbinomlem3  17193  drngnidl  17877  gsummoncoe1  18346  cnsubrg  18478  pmatcoe1fsupp  19202  mp2pm2mplem4  19310  en2top  19487  fctop  19505  cctop  19507  metusttoOLD  21060  metustto  21061  pmltpclem2  21861  itg1addlem5  22107  itg10a  22117  dvne0  22412  plyeq0lem  22607  plymullem1  22611  aalioulem4  22731  aalioulem5  22732  aaliou2b  22737  ang180lem3  23143  basellem2  23355  musumsum  23468  dchrhash  23546  lgsdir2lem5  23602  rpvmasumlem  23672  rpvmasum2  23697  pntlemj  23788  tgcolg  23941  tgbtwnconn1  23962  tgbtwnconn2  23963  hlid  23993  hltr  23994  hlbtwn  23995  colmid  24065  lmieu  24150  lmiinv  24158  clwlkisclwwlklem2a  24785  eupath2lem2  24978  3vfriswmgralem  25004  frgrawopreg  25049  2spotdisj  25061  2spotiundisj  25062  2spotmdisj  25068  frgrareg  25117  ex-natded5.7  25132  ex-natded5.13  25136  ex-natded9.20  25138  ex-natded9.20-2  25139  esumsn  28072  meascnbl  28190  signsplypnf  28507  signstfvn  28526  binomfallfaclem2  29162  sltres  29424  nobndup  29460  dfrdg4  29600  outsideoftr  29779  lineunray  29797  dvtanlem  30064  ftc1anclem3  30092  dvasin  30103  areacirclem4  30110  smprngopr  30449  tsbi1  30540  tsbi2  30541  pell1234qrdich  30797  acongtr  30916  acongrep  30918  jm2.23  30938  jm2.25  30941  fnwe2lem3  30998  kelac2lem  31010  refsum2cnlem1  31412  fmul01lt1lem1  31578  limciccioolb  31627  sumnnodd  31636  limcicciooub  31643  wallispilem3  31849  fourierdlem35  31924  fourierdlem80  31969  fourierdlem101  31990  fourierswlem  32013  etransclem32  32049  etransclem35  32052  2reu4a  32194  otiunsndisjX  32301  usgvad2edg  32411  altgsumbcALT  32942  lindslinindsimp1  33058  lindszr  33070  zlmodzxznm  33098  bj-animorr  34151  bj-animorlr  34152  lkrshpor  34832  cdleme22b  36067  tendoex  36701  lcfrlem9  37277
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
  Copyright terms: Public domain W3C validator