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 26652. (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 196  df-or 384
This theorem is referenced by:  pm2.48  414  pm2.49  415  animorr  505  animorlr  506  orim12i  537  pm1.5  543  cases2  1005  eqoreldifOLD  4173  n0snor2el  4304  propeqop  4895  somin1  5448  soxp  7177  fowdom  8359  unxpwdom2  8376  fin1a2lem11  9115  axdc3lem2  9156  gchdomtri  9330  hargch  9374  alephgch  9375  nn1m1nn  10917  nn01to3  11657  rpneg  11739  ltpnf  11830  mnflt  11833  xrlttri  11848  xmulpnf1  11976  iccsplit  12176  elfznelfzo  12439  addmodlteq  12607  bc0k  12960  bcpasc  12970  hashv01gt1  12995  hashrabsn01  13023  hashsn01  13065  hashf1  13098  pr2pwpr  13116  hashtpg  13121  ffz0iswrd  13187  ccatsymb  13219  s3sndisj  13554  s3iunsndisj  13555  fsum  14298  fsumsplit  14318  fprod  14510  binomfallfaclem2  14610  fsumdvds  14868  pwp1fsum  14952  lcmfunsnlem1  15188  lcmfunsnlem2  15191  ncoprmlnprm  15274  sumhash  15438  4sqlem17  15503  vdwlem6  15528  ram0  15564  cshwsidrepswmod0  15639  cshwsdisj  15643  mreexfidimd  16134  sgrp2nmndlem5  17239  psgnunilem1  17736  psgnunilem5  17737  gsummulg  18165  srgbinomlem3  18365  drngnidl  19050  gsummoncoe1  19495  cnsubrg  19625  pmatcoe1fsupp  20325  mp2pm2mplem4  20433  en2top  20600  fctop  20618  cctop  20620  metustto  22168  pmltpclem2  23025  itg1addlem5  23273  itg10a  23283  dvne0  23578  plyeq0lem  23770  plymullem1  23774  aalioulem4  23894  aalioulem5  23895  aaliou2b  23900  relogbf  24329  logblog  24330  ang180lem3  24341  basellem2  24608  musumsum  24718  dchrhash  24796  lgsdir2lem5  24854  rpvmasumlem  24976  rpvmasum2  25001  pntlemj  25092  tgcolg  25249  tgbtwnconn1  25270  tgbtwnconn2  25271  hlid  25304  hltr  25305  hlbtwn  25306  lnhl  25310  colmid  25383  hlpasch  25448  lmieu  25476  lmiinv  25484  cgrahl  25518  cgracol  25519  inaghl  25531  uhgrstrrepelem  25744  clwlkisclwwlklem2a  26313  eupath2lem2  26505  3vfriswmgralem  26531  frgrawopreg  26576  2spotdisj  26588  2spotiundisj  26589  2spotmdisj  26595  frgrareg  26644  ex-natded5.7  26660  ex-natded5.13  26664  ex-natded9.20  26666  ex-natded9.20-2  26667  aevdemo  26709  f1ocnt  28946  esumsnf  29453  meascnbl  29609  signsplypnf  29953  signstfvn  29972  sltres  31061  nobndup  31099  dfrdg4  31228  outsideoftr  31406  lineunray  31424  lindsdom  32573  ftc1anclem3  32657  dvasin  32666  areacirclem4  32673  smprngopr  33021  tsbi1  33110  tsbi2  33111  lkrshpor  33412  cdleme22b  34647  tendoex  35281  lcfrlem9  35857  pell1234qrdich  36443  acongtr  36563  acongrep  36565  jm2.23  36581  jm2.25  36584  fnwe2lem3  36640  kelac2lem  36652  ifpim23g  36859  frege122d  37071  clsk1indlem3  37361  refsum2cnlem1  38219  eliuniincex  38323  eliincex  38324  fmul01lt1lem1  38651  limciccioolb  38688  sumnnodd  38697  limcicciooub  38704  wallispilem3  38960  fourierdlem35  39035  fourierdlem80  39079  fourierdlem101  39100  fourierswlem  39123  etransclem32  39159  etransclem35  39162  nnfoctbdjlem  39348  2reu4a  39838  nltle2tri  39942  icceuelpartlem  39973  lighneallem3  40062  evennodd  40094  oddneven  40095  otiunsndisjX  40317  umgrvad2edg  40440  nbgrnvtx0  40563  2wspdisj  41165  2wspiundisj  41166  clwlkclwwlklem2a  41207  clwwlksnfi  41220  eupth2lem2  41387  frgrwopreg  41486  2wspmdisj  41501  av-frgrareg  41548  altgsumbcALT  41924  lindslinindsimp1  42040  lindszr  42052  zlmodzxznm  42080  elfzolborelfzop1  42103  blen1b  42180
  Copyright terms: Public domain W3C validator