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

Theorem olcd 873
Description: Deduction introducing a disjunct. A translation of natural deduction rule IL ( insertion left), see natded 29389. (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 872 . 2 (𝜑 → (𝜓𝜒))
32orcomd 870 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846
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 206  df-or 847
This theorem is referenced by:  pm2.48  884  pm2.49  885  orim12i  908  pm1.5  919  animorr  978  animorlr  979  cases2ALT  1048  2nreu  4406  2reu4lem  4488  n0snor2el  4796  disjord  5098  propeqop  5469  somin1  6092  nf1const  7255  soxp  8066  xpord2indlem  8084  naddcllem  8627  fowdom  9514  unxpwdom2  9531  nelaneq  9542  djuunxp  9864  fin1a2lem11  10353  axdc3lem2  10394  gchdomtri  10572  hargch  10616  alephgch  10617  nn1m1nn  12181  nn01to3  12873  rpneg  12954  ltpnf  13048  mnflt  13051  xrlttri  13065  xmulpnf1  13200  iccsplit  13409  elfznelfzo  13684  addmodlteq  13858  bc0k  14218  bcpasc  14228  hashv01gt1  14252  hashrabsn01  14280  hashsn01  14323  pr2pwpr  14385  hashtpg  14391  ccatsymb  14477  s3sndisj  14859  s3iunsndisj  14860  fsum  15612  fsumsplit  15633  fprod  15831  binomfallfaclem2  15930  fsumdvds  16197  pwp1fsum  16280  lcmfunsnlem1  16520  lcmfunsnlem2  16523  2mulprm  16576  ncoprmlnprm  16610  4sqlem17  16840  vdwlem6  16865  ram0  16901  cshwsidrepswmod0  16974  cshwsdisj  16978  basprssdmsets  17103  mreexfidimd  17537  homffval  17577  comfffval  17585  natfval  17840  xpchomfval  18074  xpccofval  18077  plusffval  18510  efmndplusg  18697  smndex1mgm  18724  sgrp2nmndlem5  18746  grpsubfval  18801  grpsubfvalALT  18802  psgnunilem1  19282  psgnunilem5  19283  gsummulg  19726  prmgrpsimpgd  19900  srgbinomlem3  19966  scaffval  20356  drngnidl  20715  cnsubrg  20873  ipffval  21068  psrmulr  21368  pmatcoe1fsupp  22066  en2top  22351  fctop  22370  cctop  22372  metustto  23925  pcofval  24389  pmltpclem2  24829  itg1addlem5  25081  itg10a  25091  dvne0  25391  plyeq0lem  25587  plymullem1  25591  aalioulem4  25711  aalioulem5  25712  aaliou2b  25717  ang180lem3  26177  basellem2  26447  musumsum  26557  dchrhash  26635  lgsdir2lem5  26693  rpvmasumlem  26851  rpvmasum2  26876  pntlemj  26967  sltres  27026  noetainflem4  27104  addsval  27296  mulsval  27396  tgbtwnconn1  27559  tgbtwnconn2  27560  hlid  27593  hltr  27594  hlbtwn  27595  lnhl  27599  colmid  27672  hlpasch  27740  lmieu  27768  lmiinv  27776  cgrahl  27811  cgracol  27812  inaghl  27829  edglnl  28136  umgrvad2edg  28203  nbgrnvtx0  28329  wwlksnfi  28893  clwlkclwwlklem2a  28984  clwwlknnn  29019  clwwlknon1nloop  29085  eupth2lem2  29205  frgrwopreg  29309  2wspmdisj  29323  frgrreg  29380  ex-natded5.7  29397  ex-natded5.13  29401  ex-natded9.20  29403  ex-natded9.20-2  29404  aevdemo  29446  f1ocnt  31747  linds2eq  32208  esumsnf  32703  meascnbl  32858  signsplypnf  33202  hashreprin  33273  circlemeth  33293  satfvsucsuc  33999  fmlasucdisj  34033  satfun  34045  satfv1fvfmla1  34057  2goelgoanfmla1  34058  dfrdg4  34565  outsideoftr  34743  lineunray  34761  lindsdom  36101  ftc1anclem3  36182  dvasin  36191  areacirclem4  36198  smprngopr  36540  tsbi1  36621  tsbi2  36622  lkrshpor  37598  cdleme22b  38833  tendoex  39467  lcfrlem9  40042  aks6d1c2p2  40578  pell1234qrdich  41213  acongtr  41331  acongrep  41333  jm2.23  41349  jm2.25  41352  fnwe2lem3  41408  kelac2lem  41420  mendplusgfval  41541  mendmulrfval  41543  onmcl  41695  fzunt  41801  fzuntd  41802  fzunt1d  41803  fzuntgd  41804  ifpim23g  41841  frege122d  42106  clsk1indlem3  42389  refsum2cnlem1  43316  disjxp1  43351  eliuniincex  43393  eliincex  43394  fmul01lt1lem1  43899  limciccioolb  43936  sumnnodd  43945  limcicciooub  43952  wallispilem3  44382  fourierdlem35  44457  fourierdlem80  44501  fourierdlem101  44522  fourierswlem  44545  etransclem32  44581  etransclem35  44584  nnfoctbdjlem  44770  otiunsndisjX  45585  nltle2tri  45619  icceuelpartlem  45701  lighneallem3  45873  evennodd  45909  oddneven  45910  isomuspgrlem1  46093  altgsumbcALT  46503  lindslinindsimp1  46612  lindszr  46624  zlmodzxznm  46652  elfzolborelfzop1  46674  blen1b  46748  reorelicc  46870  prelrrx2b  46874  inlinecirc02plem  46946  fvconst0ci  46999
  Copyright terms: Public domain W3C validator