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

Theorem olcd 408
 Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IL (∨ insertion left), see natded 27127. (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 407 . 2 (𝜑 → (𝜓𝜒))
32orcomd 403 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383 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 385 This theorem is referenced by:  pm2.48  415  pm2.49  416  animorr  506  animorlr  507  orim12i  538  pm1.5  544  cases2  992  eqoreldifOLD  4202  n0snor2el  4337  propeqop  4935  somin1  5493  soxp  7242  fowdom  8427  unxpwdom2  8444  fin1a2lem11  9183  axdc3lem2  9224  gchdomtri  9402  hargch  9446  alephgch  9447  nn1m1nn  10991  nn01to3  11732  rpneg  11814  ltpnf  11905  mnflt  11908  xrlttri  11923  xmulpnf1  12054  iccsplit  12254  elfznelfzo  12521  addmodlteq  12692  bc0k  13045  bcpasc  13055  hashv01gt1  13080  hashrabsn01  13109  hashsn01  13151  hashf1  13186  pr2pwpr  13206  hashtpg  13212  ffz0iswrd  13278  ccatsymb  13312  s3sndisj  13647  s3iunsndisj  13648  fsum  14391  fsumsplit  14411  fprod  14603  binomfallfaclem2  14703  fsumdvds  14961  pwp1fsum  15045  lcmfunsnlem1  15281  lcmfunsnlem2  15284  ncoprmlnprm  15367  sumhash  15531  4sqlem17  15596  vdwlem6  15621  ram0  15657  cshwsidrepswmod0  15732  cshwsdisj  15736  basprssdmsets  15853  mreexfidimd  16239  sgrp2nmndlem5  17344  psgnunilem1  17841  psgnunilem5  17842  gsummulg  18270  srgbinomlem3  18470  drngnidl  19157  gsummoncoe1  19602  cnsubrg  19734  pmatcoe1fsupp  20434  mp2pm2mplem4  20542  en2top  20709  fctop  20727  cctop  20729  metustto  22277  pmltpclem2  23137  itg1addlem5  23386  itg10a  23396  dvne0  23691  plyeq0lem  23883  plymullem1  23887  aalioulem4  24007  aalioulem5  24008  aaliou2b  24013  relogbf  24442  logblog  24443  ang180lem3  24454  basellem2  24721  musumsum  24831  dchrhash  24909  lgsdir2lem5  24967  rpvmasumlem  25089  rpvmasum2  25114  pntlemj  25205  tgcolg  25362  tgbtwnconn1  25383  tgbtwnconn2  25384  hlid  25417  hltr  25418  hlbtwn  25419  lnhl  25423  colmid  25496  hlpasch  25561  lmieu  25589  lmiinv  25597  cgrahl  25631  cgracol  25632  inaghl  25644  umgrvad2edg  26011  nbgrnvtx0  26137  2wspdisj  26736  2wspiundisj  26737  clwlkclwwlklem2a  26779  clwwlksnfi  26792  eupth2lem2  26958  frgrwopreg  27057  2wspmdisj  27072  frgrreg  27119  ex-natded5.7  27135  ex-natded5.13  27139  ex-natded9.20  27141  ex-natded9.20-2  27142  aevdemo  27184  f1ocnt  29418  esumsnf  29925  meascnbl  30081  signsplypnf  30425  signstfvn  30444  sltres  31545  nobndup  31590  dfrdg4  31727  outsideoftr  31905  lineunray  31923  lindsdom  33062  ftc1anclem3  33146  dvasin  33155  areacirclem4  33162  smprngopr  33510  tsbi1  33599  tsbi2  33600  lkrshpor  33901  cdleme22b  35136  tendoex  35770  lcfrlem9  36346  pell1234qrdich  36932  acongtr  37052  acongrep  37054  jm2.23  37070  jm2.25  37073  fnwe2lem3  37129  kelac2lem  37141  ifpim23g  37348  frege122d  37560  clsk1indlem3  37850  refsum2cnlem1  38706  eliuniincex  38804  eliincex  38805  fmul01lt1lem1  39243  limciccioolb  39280  sumnnodd  39289  limcicciooub  39296  wallispilem3  39612  fourierdlem35  39687  fourierdlem80  39731  fourierdlem101  39752  fourierswlem  39775  etransclem32  39811  etransclem35  39814  nnfoctbdjlem  40000  2reu4a  40514  otiunsndisjX  40616  nltle2tri  40641  icceuelpartlem  40690  lighneallem3  40844  evennodd  40876  oddneven  40877  altgsumbcALT  41440  lindslinindsimp1  41555  lindszr  41567  zlmodzxznm  41595  elfzolborelfzop1  41618  blen1b  41695
 Copyright terms: Public domain W3C validator