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

Theorem olcd 890
Description: Deduction introducing a disjunct. A translation of natural deduction rule IL ( insertion left), see natded 27619. (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 889 . 2 (𝜑 → (𝜓𝜒))
32orcomd 887 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 863
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 198  df-or 864
This theorem is referenced by:  pm2.48  898  pm2.49  899  orim12i  921  pm1.5  932  animorr  990  animorlr  991  cases2ALT  1060  n0snor2el  4508  disjord  4786  propeqop  5114  somin1  5681  soxp  7462  fowdom  8653  unxpwdom2  8670  nelaneq  8681  djuunxp  8968  fin1a2lem11  9455  axdc3lem2  9496  gchdomtri  9674  hargch  9718  alephgch  9719  nn1m1nn  11263  nn01to3  12006  rpneg  12083  ltpnf  12176  mnflt  12179  xrlttri  12194  xmulpnf1  12328  iccsplit  12534  elfznelfzo  12803  addmodlteq  12975  bc0k  13324  bcpasc  13334  hashv01gt1  13359  hashrabsn01  13386  hashsn01  13428  hashf1  13465  pr2pwpr  13485  hashtpg  13491  ffz0iswrd  13550  ccatsymb  13586  s3sndisj  13938  s3iunsndisj  13939  fsum  14681  fsumsplit  14701  fprod  14900  binomfallfaclem2  14999  fsumdvds  15261  pwp1fsum  15344  lcmfunsnlem1  15579  lcmfunsnlem2  15582  ncoprmlnprm  15663  sumhash  15827  4sqlem17  15892  vdwlem6  15917  ram0  15953  cshwsidrepswmod0  16028  cshwsdisj  16032  basprssdmsets  16152  mreexfidimd  16538  sgrp2nmndlem5  17644  psgnunilem1  18140  psgnunilem5  18141  gsummulg  18569  srgbinomlem3  18770  drngnidl  19464  cnsubrg  20041  pmatcoe1fsupp  20746  mp2pm2mplem4  20854  en2top  21030  fctop  21049  cctop  21051  metustto  22598  pmltpclem2  23457  itg1addlem5  23708  itg10a  23718  dvne0  24015  plyeq0lem  24207  plymullem1  24211  aalioulem4  24331  aalioulem5  24332  aaliou2b  24337  relogbf  24771  logblog  24772  ang180lem3  24783  basellem2  25050  musumsum  25160  dchrhash  25238  lgsdir2lem5  25296  rpvmasumlem  25418  rpvmasum2  25443  pntlemj  25534  tgcolg  25691  tgbtwnconn1  25712  tgbtwnconn2  25713  hlid  25746  hltr  25747  hlbtwn  25748  lnhl  25752  colmid  25825  hlpasch  25890  lmieu  25918  lmiinv  25926  cgrahl  25960  cgracol  25961  inaghl  25973  edglnl  26281  umgrvad2edg  26348  nbgrnvtx0  26476  clwlkclwwlklem2a  27169  clwwlknnn  27209  clwwlknfi  27222  clwwlknon1nloop  27295  eupth2lem2  27420  frgrwopreg  27526  2wspmdisj  27540  frgrreg  27610  ex-natded5.7  27627  ex-natded5.13  27631  ex-natded9.20  27633  ex-natded9.20-2  27634  aevdemo  27676  f1ocnt  29916  esumsnf  30483  meascnbl  30639  signsplypnf  30984  signstfvn  31003  hashreprin  31055  circlemeth  31075  sltres  32169  dfrdg4  32412  outsideoftr  32590  lineunray  32608  lindsdom  33753  ftc1anclem3  33836  dvasin  33845  areacirclem4  33852  smprngopr  34199  tsbi1  34288  tsbi2  34289  lkrshpor  34931  cdleme22b  36166  tendoex  36800  lcfrlem9  37375  pell1234qrdich  37966  acongtr  38086  acongrep  38088  jm2.23  38104  jm2.25  38107  fnwe2lem3  38163  kelac2lem  38175  ifpim23g  38380  frege122d  38592  clsk1indlem3  38881  refsum2cnlem1  39730  eliuniincex  39825  eliincex  39826  fmul01lt1lem1  40340  limciccioolb  40377  sumnnodd  40386  limcicciooub  40393  wallispilem3  40807  fourierdlem35  40882  fourierdlem80  40926  fourierdlem101  40947  fourierswlem  40970  etransclem32  41006  etransclem35  41009  nnfoctbdjlem  41195  2reu4a  41734  otiunsndisjX  41845  nltle2tri  41875  icceuelpartlem  41923  lighneallem3  42076  evennodd  42108  oddneven  42109  altgsumbcALT  42683  lindslinindsimp1  42798  lindszr  42810  zlmodzxznm  42838  elfzolborelfzop1  42861  blen1b  42934
  Copyright terms: Public domain W3C validator