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

Theorem olcd 407
Description: Deduction introducing a disjunct. A translation of natural deduction rule IL ( insertion left), see natded 27390. (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 406 . 2 (𝜑 → (𝜓𝜒))
32orcomd 402 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382
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 384
This theorem is referenced by:  pm2.48  414  pm2.49  415  animorr  505  animorlr  506  orim12i  537  pm1.5  543  cases2ALT  1017  eqoreldifOLD  4258  n0snor2el  4396  disjord  4673  propeqop  4999  somin1  5564  soxp  7335  fowdom  8517  unxpwdom2  8534  fin1a2lem11  9270  axdc3lem2  9311  gchdomtri  9489  hargch  9533  alephgch  9534  nn1m1nn  11078  nn01to3  11819  rpneg  11901  ltpnf  11992  mnflt  11995  xrlttri  12010  xmulpnf1  12142  iccsplit  12343  elfznelfzo  12613  addmodlteq  12785  bc0k  13138  bcpasc  13148  hashv01gt1  13173  hashrabsn01  13200  hashsn01  13242  hashf1  13279  pr2pwpr  13299  hashtpg  13305  ffz0iswrd  13364  ccatsymb  13400  s3sndisj  13752  s3iunsndisj  13753  fsum  14495  fsumsplit  14515  fprod  14715  binomfallfaclem2  14815  fsumdvds  15077  pwp1fsum  15161  lcmfunsnlem1  15397  lcmfunsnlem2  15400  ncoprmlnprm  15483  sumhash  15647  4sqlem17  15712  vdwlem6  15737  ram0  15773  cshwsidrepswmod0  15848  cshwsdisj  15852  basprssdmsets  15972  mreexfidimd  16358  sgrp2nmndlem5  17463  psgnunilem1  17959  psgnunilem5  17960  gsummulg  18388  srgbinomlem3  18588  drngnidl  19277  gsummoncoe1  19722  cnsubrg  19854  pmatcoe1fsupp  20554  mp2pm2mplem4  20662  en2top  20837  fctop  20856  cctop  20858  metustto  22405  pmltpclem2  23264  itg1addlem5  23512  itg10a  23522  dvne0  23819  plyeq0lem  24011  plymullem1  24015  aalioulem4  24135  aalioulem5  24136  aaliou2b  24141  relogbf  24574  logblog  24575  ang180lem3  24586  basellem2  24853  musumsum  24963  dchrhash  25041  lgsdir2lem5  25099  rpvmasumlem  25221  rpvmasum2  25246  pntlemj  25337  tgcolg  25494  tgbtwnconn1  25515  tgbtwnconn2  25516  hlid  25549  hltr  25550  hlbtwn  25551  lnhl  25555  colmid  25628  hlpasch  25693  lmieu  25721  lmiinv  25729  cgrahl  25763  cgracol  25764  inaghl  25776  edglnl  26083  umgrvad2edg  26150  nbgrnvtx0  26277  clwlkclwwlklem2a  26964  clwwlknnn  26995  clwwlknfi  27008  clwwlknon1nloop  27074  eupth2lem2  27197  frgrwopreg  27303  2wspmdisj  27317  frgrreg  27381  ex-natded5.7  27398  ex-natded5.13  27402  ex-natded9.20  27404  ex-natded9.20-2  27405  aevdemo  27447  f1ocnt  29687  esumsnf  30254  meascnbl  30410  signsplypnf  30755  signstfvn  30774  hashreprin  30826  circlemeth  30846  sltres  31940  dfrdg4  32183  outsideoftr  32361  lineunray  32379  lindsdom  33533  ftc1anclem3  33617  dvasin  33626  areacirclem4  33633  smprngopr  33981  tsbi1  34070  tsbi2  34071  lkrshpor  34712  cdleme22b  35946  tendoex  36580  lcfrlem9  37156  pell1234qrdich  37742  acongtr  37862  acongrep  37864  jm2.23  37880  jm2.25  37883  fnwe2lem3  37939  kelac2lem  37951  ifpim23g  38157  frege122d  38369  clsk1indlem3  38658  refsum2cnlem1  39510  eliuniincex  39606  eliincex  39607  fmul01lt1lem1  40134  limciccioolb  40171  sumnnodd  40180  limcicciooub  40187  wallispilem3  40602  fourierdlem35  40677  fourierdlem80  40721  fourierdlem101  40742  fourierswlem  40765  etransclem32  40801  etransclem35  40804  nnfoctbdjlem  40990  2reu4a  41510  otiunsndisjX  41621  nltle2tri  41648  icceuelpartlem  41696  lighneallem3  41849  evennodd  41881  oddneven  41882  altgsumbcALT  42456  lindslinindsimp1  42571  lindszr  42583  zlmodzxznm  42611  elfzolborelfzop1  42634  blen1b  42707
  Copyright terms: Public domain W3C validator