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

Theorem olcd 393
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 25251. (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 392 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 388 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  pm2.48  400  pm2.49  401  orim12i  516  pm1.5  522  cases2  971  otsndisj  4761  otiunsndisj  4762  somin1  5410  soxp  6912  fowdom  8015  unxpwdom2  8032  fin1a2lem11  8807  axdc3lem2  8848  gchdomtri  9024  hargch  9068  alephgch  9069  nn1m1nn  10576  nn01to3  11200  rpneg  11274  ltpnf  11356  mnflt  11358  xrlttri  11370  xmulpnf1  11491  iccsplit  11678  elfznelfzo  11918  bc0k  12392  bcpasc  12402  hashv01gt1  12421  hashrabsn01  12444  hashf1  12510  pr2pwpr  12524  hashtpg  12527  ffz0iswrd  12576  ccatsymb  12609  fsum  13554  fsumsplit  13574  fprod  13760  fsumdvds  14041  sumhash  14427  4sqlem17  14491  vdwlem6  14516  ram0  14552  cshwsidrepswmod0  14591  cshwsdisj  14595  mreexfidimd  15067  sgrp2nmndlem5  16174  psgnunilem1  16645  psgnunilem5  16646  gsummulg  17092  srgbinomlem3  17320  drngnidl  18004  gsummoncoe1  18473  cnsubrg  18605  pmatcoe1fsupp  19329  mp2pm2mplem4  19437  en2top  19614  fctop  19632  cctop  19634  metusttoOLD  21186  metustto  21187  pmltpclem2  21987  itg1addlem5  22233  itg10a  22243  dvne0  22538  plyeq0lem  22733  plymullem1  22737  aalioulem4  22857  aalioulem5  22858  aaliou2b  22863  ang180lem3  23269  basellem2  23481  musumsum  23594  dchrhash  23672  lgsdir2lem5  23728  rpvmasumlem  23798  rpvmasum2  23823  pntlemj  23914  tgcolg  24067  tgbtwnconn1  24088  tgbtwnconn2  24089  hlid  24119  hltr  24120  hlbtwn  24121  colmid  24191  lmieu  24276  lmiinv  24284  clwlkisclwwlklem2a  24912  eupath2lem2  25105  3vfriswmgralem  25131  frgrawopreg  25176  2spotdisj  25188  2spotiundisj  25189  2spotmdisj  25195  frgrareg  25244  ex-natded5.7  25259  ex-natded5.13  25263  ex-natded9.20  25265  ex-natded9.20-2  25266  esumsnf  28236  meascnbl  28363  signsplypnf  28704  signstfvn  28723  binomfallfaclem2  29359  sltres  29620  nobndup  29656  dfrdg4  29784  outsideoftr  29963  lineunray  29981  dvtanlem  30248  ftc1anclem3  30276  dvasin  30287  areacirclem4  30294  smprngopr  30633  tsbi1  30724  tsbi2  30725  pell1234qrdich  30980  acongtr  31099  acongrep  31101  jm2.23  31121  jm2.25  31124  fnwe2lem3  31181  kelac2lem  31193  refsum2cnlem1  31594  fmul01lt1lem1  31760  limciccioolb  31809  sumnnodd  31818  limcicciooub  31825  wallispilem3  32031  fourierdlem35  32106  fourierdlem80  32151  fourierdlem101  32172  fourierswlem  32195  etransclem32  32231  etransclem35  32234  2reu4a  32376  otiunsndisjX  32544  usgvad2edg  32652  altgsumbcALT  33065  lindslinindsimp1  33181  lindszr  33193  zlmodzxznm  33221  bj-animorr  34273  bj-animorlr  34274  lkrshpor  34954  cdleme22b  36189  tendoex  36823  lcfrlem9  37399
  Copyright terms: Public domain W3C validator