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

Theorem olcd 874
Description: Deduction introducing a disjunct. A translation of natural deduction rule IL ( insertion left), see natded 28491. (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 873 . 2 (𝜑 → (𝜓𝜒))
32orcomd 871 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847
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 210  df-or 848
This theorem is referenced by:  pm2.48  885  pm2.49  886  orim12i  909  pm1.5  920  animorr  979  animorlr  980  cases2ALT  1049  2nreu  4361  2reu4lem  4442  n0snor2el  4749  disjord  5046  propeqop  5395  somin1  6003  nf1const  7119  soxp  7901  fowdom  9192  unxpwdom2  9209  nelaneq  9220  djuunxp  9542  fin1a2lem11  10029  axdc3lem2  10070  gchdomtri  10248  hargch  10292  alephgch  10293  nn1m1nn  11856  nn01to3  12542  rpneg  12623  ltpnf  12717  mnflt  12720  xrlttri  12734  xmulpnf1  12869  iccsplit  13078  elfznelfzo  13352  addmodlteq  13524  bc0k  13882  bcpasc  13892  hashv01gt1  13916  hashrabsn01  13945  hashsn01  13988  pr2pwpr  14050  hashtpg  14056  ccatsymb  14144  s3sndisj  14535  s3iunsndisj  14536  fsum  15289  fsumsplit  15310  fprod  15508  binomfallfaclem2  15607  fsumdvds  15874  pwp1fsum  15957  lcmfunsnlem1  16199  lcmfunsnlem2  16202  2mulprm  16255  ncoprmlnprm  16289  4sqlem17  16519  vdwlem6  16544  ram0  16580  cshwsidrepswmod0  16653  cshwsdisj  16657  basprssdmsets  16777  mreexfidimd  17158  homffval  17198  comfffval  17206  natfval  17458  xpchomfval  17691  xpccofval  17694  plusffval  18125  efmndplusg  18312  smndex1mgm  18339  sgrp2nmndlem5  18361  grpsubfval  18416  grpsubfvalALT  18417  psgnunilem1  18890  psgnunilem5  18891  gsummulg  19332  prmgrpsimpgd  19506  srgbinomlem3  19562  scaffval  19922  drngnidl  20272  cnsubrg  20428  ipffval  20615  psrmulr  20914  pmatcoe1fsupp  21603  en2top  21887  fctop  21906  cctop  21908  metustto  23456  pcofval  23912  pmltpclem2  24351  itg1addlem5  24603  itg10a  24613  dvne0  24913  plyeq0lem  25109  plymullem1  25113  aalioulem4  25233  aalioulem5  25234  aaliou2b  25239  ang180lem3  25699  basellem2  25969  musumsum  26079  dchrhash  26157  lgsdir2lem5  26215  rpvmasumlem  26373  rpvmasum2  26398  pntlemj  26489  tgbtwnconn1  26671  tgbtwnconn2  26672  hlid  26705  hltr  26706  hlbtwn  26707  lnhl  26711  colmid  26784  hlpasch  26852  lmieu  26880  lmiinv  26888  cgrahl  26923  cgracol  26924  inaghl  26941  edglnl  27239  umgrvad2edg  27306  nbgrnvtx0  27432  wwlksnfi  27995  clwlkclwwlklem2a  28086  clwwlknnn  28121  clwwlknon1nloop  28187  eupth2lem2  28307  frgrwopreg  28411  2wspmdisj  28425  frgrreg  28482  ex-natded5.7  28499  ex-natded5.13  28503  ex-natded9.20  28505  ex-natded9.20-2  28506  aevdemo  28548  f1ocnt  30848  linds2eq  31294  esumsnf  31749  meascnbl  31904  signsplypnf  32246  hashreprin  32317  circlemeth  32337  satfvsucsuc  33045  fmlasucdisj  33079  satfun  33091  satfv1fvfmla1  33103  2goelgoanfmla1  33104  xpord2ind  33536  naddcllem  33573  sltres  33607  noetainflem4  33685  addsval  33868  dfrdg4  33995  outsideoftr  34173  lineunray  34191  lindsdom  35513  ftc1anclem3  35594  dvasin  35603  areacirclem4  35610  smprngopr  35952  tsbi1  36033  tsbi2  36034  lkrshpor  36863  cdleme22b  38097  tendoex  38731  lcfrlem9  39306  pell1234qrdich  40394  acongtr  40511  acongrep  40513  jm2.23  40529  jm2.25  40532  fnwe2lem3  40588  kelac2lem  40600  mendplusgfval  40721  mendmulrfval  40723  ifpim23g  40795  frege122d  41053  clsk1indlem3  41338  refsum2cnlem1  42261  disjxp1  42298  eliuniincex  42340  eliincex  42341  fmul01lt1lem1  42808  limciccioolb  42845  sumnnodd  42854  limcicciooub  42861  wallispilem3  43291  fourierdlem35  43366  fourierdlem80  43410  fourierdlem101  43431  fourierswlem  43454  etransclem32  43490  etransclem35  43493  nnfoctbdjlem  43676  otiunsndisjX  44451  nltle2tri  44486  icceuelpartlem  44568  lighneallem3  44740  evennodd  44776  oddneven  44777  isomuspgrlem1  44960  altgsumbcALT  45370  lindslinindsimp1  45479  lindszr  45491  zlmodzxznm  45519  elfzolborelfzop1  45541  blen1b  45615  reorelicc  45737  prelrrx2b  45741  inlinecirc02plem  45813  fvconst0ci  45867
  Copyright terms: Public domain W3C validator