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

Theorem olcd 382
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 20790. (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 381 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 377 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  pm2.48  389  pm2.49  390  orim12i  502  pm1.5  508  somin1  5079  soxp  6228  fowdom  7285  unxpwdom2  7302  fin1a2lem11  8036  axdc3lem2  8077  gchdomtri  8251  hargch  8299  alephgch  8300  nn1m1nn  9766  nnnegz  10027  rpneg  10383  ltpnf  10463  mnflt  10464  xrlttri  10473  xmulpnf1  10594  iccsplit  10768  bcpasc  11333  hashf1  11395  fsum  12193  fsumsplit  12212  fsumdvds  12572  sumhash  12944  4sqlem17  13008  vdwlem6  13033  0hashbc  13054  ram0  13069  mreexfidimd  13552  gsummulg  15214  drngnidl  15981  cnsubrg  16432  en2top  16723  fctop  16741  cctop  16743  pmltpclem2  18809  itg1addlem5  19055  itg10a  19065  dvne0  19358  plyeq0lem  19592  plymullem1  19596  aalioulem4  19715  aalioulem5  19716  aaliou2b  19721  ang180lem3  20109  basellem2  20319  musumsum  20432  dchrhash  20510  lgsdir2lem5  20566  rpvmasumlem  20636  rpvmasum2  20661  pntlemj  20752  ex-natded5.7  20798  ex-natded5.13  20802  ex-natded9.20  20804  ex-natded9.20-2  20805  esumsn  23437  meascnbl  23546  eupath2lem2  23902  sltres  24318  nobndup  24354  dfrdg4  24488  outsideoftr  24752  lineunray  24770  dvreasin  24923  areacirclem5  24929  evpexun  24998  hdrmp  25706  partarelt2  25897  smprngopr  26677  pell1234qrdich  26946  acongtr  27065  acongrep  27067  jm2.23  27089  jm2.25  27092  fnwe2lem3  27149  kelac2lem  27162  psgnunilem1  27416  psgnunilem5  27417  refsum2cnlem1  27708  fmul01lt1lem1  27714  stoweidlem1  27750  wallispilem3  27816  2reu4a  27967  nbusgra  28143  frgra2v  28177  3vfriswmgralem  28182  lkrshpor  29297  cdleme22b  30530  tendoex  31164  lcfrlem9  31740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator