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

Theorem olcd 399
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 25901. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
Hypothesis
Ref Expression
orcd.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
olcd  |-  ( ph  ->  ( ch  \/  ps ) )

Proof of Theorem olcd
StepHypRef Expression
1 orcd.1 . . 3  |-  ( ph  ->  ps )
21orcd 398 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 394 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 374
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 190  df-or 376
This theorem is referenced by:  pm2.48  406  pm2.49  407  orim12i  523  pm1.5  529  cases2  989  eqoreldif  4024  otsndisj  4719  otiunsndisj  4720  somin1  5251  soxp  6935  fowdom  8111  unxpwdom2  8128  fin1a2lem11  8865  axdc3lem2  8906  gchdomtri  9079  hargch  9123  alephgch  9124  nn1m1nn  10656  nn01to3  11285  rpneg  11360  ltpnf  11450  mnflt  11453  xrlttri  11466  xmulpnf1  11588  iccsplit  11793  elfznelfzo  12044  bc0k  12527  bcpasc  12537  hashv01gt1  12559  hashrabsn01  12583  hashf1  12652  pr2pwpr  12668  hashtpg  12673  ffz0iswrd  12729  ccatsymb  12762  fsum  13834  fsumsplit  13854  fprod  14043  binomfallfaclem2  14141  fsumdvds  14396  lcmfunsnlem1  14658  lcmfunsnlem2  14661  ncoprmlnprm  14725  sumhash  14889  4sqlem17OLD  14953  4sqlem17  14959  vdwlem6  14984  ram0  15028  cshwsidrepswmod0  15113  cshwsdisj  15117  mreexfidimd  15604  sgrp2nmndlem5  16711  psgnunilem1  17182  psgnunilem5  17183  gsummulg  17623  srgbinomlem3  17823  drngnidl  18501  gsummoncoe1  18946  cnsubrg  19076  pmatcoe1fsupp  19773  mp2pm2mplem4  19881  en2top  20049  fctop  20067  cctop  20069  metustto  21616  pmltpclem2  22448  itg1addlem5  22706  itg10a  22716  dvne0  23011  plyeq0lem  23212  plymullem1  23216  aalioulem4  23339  aalioulem5  23340  aaliou2b  23345  relogbf  23776  logblog  23777  ang180lem3  23788  basellem2  24056  musumsum  24169  dchrhash  24247  lgsdir2lem5  24303  rpvmasumlem  24373  rpvmasum2  24398  pntlemj  24489  tgcolg  24647  tgbtwnconn1  24668  tgbtwnconn2  24669  hlid  24702  hltr  24703  hlbtwn  24704  lnhl  24708  colmid  24781  hlpasch  24846  lmieu  24874  lmiinv  24882  cgrahl  24916  cgracol  24917  inaghl  24929  clwlkisclwwlklem2a  25561  eupath2lem2  25754  3vfriswmgralem  25780  frgrawopreg  25825  2spotdisj  25837  2spotiundisj  25838  2spotmdisj  25844  frgrareg  25893  ex-natded5.7  25909  ex-natded5.13  25913  ex-natded9.20  25915  ex-natded9.20-2  25916  f1ocnt  28424  esumsnf  28933  meascnbl  29089  signsplypnf  29487  signstfvn  29506  sltres  30599  nobndup  30637  dfrdg4  30766  outsideoftr  30944  lineunray  30962  bj-animorr  31190  bj-animorlr  31191  dvtanlemOLD  32035  ftc1anclem3  32063  dvasin  32072  areacirclem4  32079  smprngopr  32329  tsbi1  32419  tsbi2  32420  lkrshpor  32717  cdleme22b  33952  tendoex  34586  lcfrlem9  35162  pell1234qrdich  35751  acongtr  35872  acongrep  35874  jm2.23  35895  jm2.25  35898  fnwe2lem3  35954  kelac2lem  35966  ifpim23g  36183  frege122d  36396  refsum2cnlem1  37397  fmul01lt1lem1  37699  limciccioolb  37738  sumnnodd  37747  limcicciooub  37754  wallispilem3  37966  fourierdlem35  38042  fourierdlem80  38087  fourierdlem101  38108  fourierswlem  38131  etransclem32  38168  etransclem35  38171  2reu4a  38647  nltle2tri  38753  icceuelpartlem  38786  evennodd  38810  oddneven  38811  n0snor2el  39035  propeqop  39038  otiunsndisjX  39045  nbgrnvtx0  39458  usgvad2edg  39995  altgsumbcALT  40406  lindslinindsimp1  40522  lindszr  40534  zlmodzxznm  40562  elfzolborelfzop1  40588  blen1b  40671
  Copyright terms: Public domain W3C validator