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

Theorem olcd 870
 Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 28181. (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 869 . 2 (𝜑 → (𝜓𝜒))
32orcomd 867 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 843 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 209  df-or 844 This theorem is referenced by:  pm2.48  881  pm2.49  882  orim12i  905  pm1.5  916  animorr  975  animorlr  976  cases2ALT  1043  2nreu  4392  2reu4lem  4464  n0snor2el  4763  disjord  5053  propeqop  5396  somin1  5992  nf1const  7058  soxp  7822  fowdom  9034  unxpwdom2  9051  nelaneq  9062  djuunxp  9349  fin1a2lem11  9831  axdc3lem2  9872  gchdomtri  10050  hargch  10094  alephgch  10095  nn1m1nn  11657  nn01to3  12340  rpneg  12420  ltpnf  12514  mnflt  12517  xrlttri  12531  xmulpnf1  12666  iccsplit  12870  elfznelfzo  13141  addmodlteq  13313  bc0k  13670  bcpasc  13680  hashv01gt1  13704  hashrabsn01  13733  hashsn01  13776  pr2pwpr  13836  hashtpg  13842  ffz0iswrdOLD  13891  ccatsymb  13935  s3sndisj  14326  s3iunsndisj  14327  fsum  15076  fsumsplit  15096  fprod  15294  binomfallfaclem2  15393  fsumdvds  15657  pwp1fsum  15741  lcmfunsnlem1  15980  lcmfunsnlem2  15983  2mulprm  16036  ncoprmlnprm  16067  4sqlem17  16296  vdwlem6  16321  ram0  16357  cshwsidrepswmod0  16427  cshwsdisj  16431  basprssdmsets  16548  mreexfidimd  16920  homffval  16959  comfffval  16967  natfval  17215  xpchomfval  17428  xpccofval  17431  plusffval  17857  efmndplusg  18044  smndex1mgm  18071  sgrp2nmndlem5  18093  grpsubfval  18146  grpsubfvalALT  18147  psgnunilem1  18620  psgnunilem5  18621  gsummulg  19061  prmgrpsimpgd  19235  srgbinomlem3  19291  scaffval  19651  drngnidl  20001  psrmulr  20163  cnsubrg  20604  ipffval  20791  pmatcoe1fsupp  21308  en2top  21592  fctop  21611  cctop  21613  metustto  23162  pcofval  23613  pmltpclem2  24049  itg1addlem5  24300  itg10a  24310  dvne0  24607  plyeq0lem  24799  plymullem1  24803  aalioulem4  24923  aalioulem5  24924  aaliou2b  24929  ang180lem3  25388  basellem2  25658  musumsum  25768  dchrhash  25846  lgsdir2lem5  25904  rpvmasumlem  26062  rpvmasum2  26087  pntlemj  26178  tgbtwnconn1  26360  tgbtwnconn2  26361  hlid  26394  hltr  26395  hlbtwn  26396  lnhl  26400  colmid  26473  hlpasch  26541  lmieu  26569  lmiinv  26577  cgrahl  26612  cgracol  26613  inaghl  26630  edglnl  26927  umgrvad2edg  26994  nbgrnvtx0  27120  wwlksnfi  27683  clwlkclwwlklem2a  27775  clwwlknnn  27810  clwwlknfiOLD  27823  clwwlknon1nloop  27877  eupth2lem2  27997  frgrwopreg  28101  2wspmdisj  28115  frgrreg  28172  ex-natded5.7  28189  ex-natded5.13  28193  ex-natded9.20  28195  ex-natded9.20-2  28196  aevdemo  28238  f1ocnt  30524  linds2eq  30941  esumsnf  31323  meascnbl  31478  signsplypnf  31820  hashreprin  31891  circlemeth  31911  satfvsucsuc  32612  fmlasucdisj  32646  satfun  32658  satfv1fvfmla1  32670  2goelgoanfmla1  32671  sltres  33169  dfrdg4  33412  outsideoftr  33590  lineunray  33608  lindsdom  34885  ftc1anclem3  34968  dvasin  34977  areacirclem4  34984  smprngopr  35329  tsbi1  35410  tsbi2  35411  lkrshpor  36242  cdleme22b  37476  tendoex  38110  lcfrlem9  38685  pell1234qrdich  39456  acongtr  39573  acongrep  39575  jm2.23  39591  jm2.25  39594  fnwe2lem3  39650  kelac2lem  39662  mendplusgfval  39783  mendmulrfval  39785  ifpim23g  39859  frege122d  40103  clsk1indlem3  40391  refsum2cnlem1  41292  disjxp1  41329  eliuniincex  41373  eliincex  41374  fmul01lt1lem1  41863  limciccioolb  41900  sumnnodd  41909  limcicciooub  41916  wallispilem3  42351  fourierdlem35  42426  fourierdlem80  42470  fourierdlem101  42491  fourierswlem  42514  etransclem32  42550  etransclem35  42553  nnfoctbdjlem  42736  otiunsndisjX  43477  nltle2tri  43512  icceuelpartlem  43594  lighneallem3  43771  evennodd  43807  oddneven  43808  isomuspgrlem1  43991  altgsumbcALT  44400  lindslinindsimp1  44511  lindszr  44523  zlmodzxznm  44551  elfzolborelfzop1  44573  blen1b  44647  reorelicc  44696  prelrrx2b  44700  inlinecirc02plem  44772
 Copyright terms: Public domain W3C validator