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

Theorem olcd 863
Description: Deduction introducing a disjunct. A translation of natural deduction rule IL ( insertion left), see natded 27602. (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 862 . 2 (𝜑 → (𝜓𝜒))
32orcomd 860 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 836
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 197  df-or 837
This theorem is referenced by:  pm2.48  871  pm2.49  872  orim12i  894  pm1.5  905  animorr  963  animorlr  964  cases2ALT  1033  n0snor2el  4497  disjord  4775  propeqop  5100  somin1  5670  soxp  7441  fowdom  8632  unxpwdom2  8649  nelaneq  8660  djuunxp  8947  fin1a2lem11  9434  axdc3lem2  9475  gchdomtri  9653  hargch  9697  alephgch  9698  nn1m1nn  11242  nn01to3  11984  rpneg  12066  ltpnf  12159  mnflt  12162  xrlttri  12177  xmulpnf1  12309  iccsplit  12512  elfznelfzo  12781  addmodlteq  12953  bc0k  13302  bcpasc  13312  hashv01gt1  13337  hashrabsn01  13364  hashsn01  13406  hashf1  13443  pr2pwpr  13463  hashtpg  13469  ffz0iswrd  13528  ccatsymb  13564  s3sndisj  13916  s3iunsndisj  13917  fsum  14659  fsumsplit  14679  fprod  14878  binomfallfaclem2  14977  fsumdvds  15239  pwp1fsum  15322  lcmfunsnlem1  15558  lcmfunsnlem2  15561  ncoprmlnprm  15643  sumhash  15807  4sqlem17  15872  vdwlem6  15897  ram0  15933  cshwsidrepswmod0  16008  cshwsdisj  16012  basprssdmsets  16132  mreexfidimd  16518  sgrp2nmndlem5  17624  psgnunilem1  18120  psgnunilem5  18121  gsummulg  18549  srgbinomlem3  18750  drngnidl  19444  cnsubrg  20021  pmatcoe1fsupp  20726  mp2pm2mplem4  20834  en2top  21010  fctop  21029  cctop  21031  metustto  22578  pmltpclem2  23437  itg1addlem5  23687  itg10a  23697  dvne0  23994  plyeq0lem  24186  plymullem1  24190  aalioulem4  24310  aalioulem5  24311  aaliou2b  24316  relogbf  24750  logblog  24751  ang180lem3  24762  basellem2  25029  musumsum  25139  dchrhash  25217  lgsdir2lem5  25275  rpvmasumlem  25397  rpvmasum2  25422  pntlemj  25513  tgcolg  25670  tgbtwnconn1  25691  tgbtwnconn2  25692  hlid  25725  hltr  25726  hlbtwn  25727  lnhl  25731  colmid  25804  hlpasch  25869  lmieu  25897  lmiinv  25905  cgrahl  25939  cgracol  25940  inaghl  25952  edglnl  26260  umgrvad2edg  26327  nbgrnvtx0  26455  clwlkclwwlklem2a  27148  clwwlknnn  27188  clwwlknfi  27201  clwwlknon1nloop  27274  eupth2lem2  27399  frgrwopreg  27505  2wspmdisj  27519  frgrreg  27593  ex-natded5.7  27610  ex-natded5.13  27614  ex-natded9.20  27616  ex-natded9.20-2  27617  aevdemo  27659  f1ocnt  29899  esumsnf  30466  meascnbl  30622  signsplypnf  30967  signstfvn  30986  hashreprin  31038  circlemeth  31058  sltres  32152  dfrdg4  32395  outsideoftr  32573  lineunray  32591  lindsdom  33736  ftc1anclem3  33819  dvasin  33828  areacirclem4  33835  smprngopr  34183  tsbi1  34272  tsbi2  34273  lkrshpor  34916  cdleme22b  36150  tendoex  36784  lcfrlem9  37360  pell1234qrdich  37951  acongtr  38071  acongrep  38073  jm2.23  38089  jm2.25  38092  fnwe2lem3  38148  kelac2lem  38160  ifpim23g  38366  frege122d  38578  clsk1indlem3  38867  refsum2cnlem1  39718  eliuniincex  39813  eliincex  39814  fmul01lt1lem1  40334  limciccioolb  40371  sumnnodd  40380  limcicciooub  40387  wallispilem3  40801  fourierdlem35  40876  fourierdlem80  40920  fourierdlem101  40941  fourierswlem  40964  etransclem32  41000  etransclem35  41003  nnfoctbdjlem  41189  2reu4a  41709  otiunsndisjX  41821  nltle2tri  41851  icceuelpartlem  41899  lighneallem3  42052  evennodd  42084  oddneven  42085  altgsumbcALT  42659  lindslinindsimp1  42774  lindszr  42786  zlmodzxznm  42814  elfzolborelfzop1  42837  blen1b  42910
  Copyright terms: Public domain W3C validator