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 24829. (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  970  cases2OLD  971  otsndisj  4752  otiunsndisj  4753  somin1  5403  soxp  6896  fowdom  7997  unxpwdom2  8014  fin1a2lem11  8790  axdc3lem2  8831  gchdomtri  9007  hargch  9051  alephgch  9052  nn1m1nn  10556  nnnegz  10867  nn01to3  11175  rpneg  11249  ltpnf  11331  mnflt  11333  xrlttri  11345  xmulpnf1  11466  iccsplit  11653  elfznelfzo  11883  bc0k  12357  bcpasc  12367  hashv01gt1  12386  hashrabsn01  12409  hashf1  12472  pr2pwpr  12486  hashtpg  12489  ffz0iswrd  12534  wrdsymb0  12540  ccatsymb  12565  fsum  13505  fsumsplit  13525  fsumdvds  13888  sumhash  14274  4sqlem17  14338  vdwlem6  14363  ram0  14399  cshwsidrepswmod0  14437  cshwsdisj  14441  mreexfidimd  14905  psgnunilem1  16324  psgnunilem5  16325  gsummulg  16768  srgbinomlem3  16995  drngnidl  17676  gsummoncoe1  18145  cnsubrg  18274  pmatcoe1fsupp  18997  mp2pm2mplem4  19105  en2top  19281  fctop  19299  cctop  19301  metusttoOLD  20823  metustto  20824  pmltpclem2  21624  itg1addlem5  21870  itg10a  21880  dvne0  22175  plyeq0lem  22370  plymullem1  22374  aalioulem4  22493  aalioulem5  22494  aaliou2b  22499  ang180lem3  22899  basellem2  23111  musumsum  23224  dchrhash  23302  lgsdir2lem5  23358  rpvmasumlem  23428  rpvmasum2  23453  pntlemj  23544  tgcolg  23697  tgbtwnconn1  23717  tgbtwnconn2  23718  colmid  23801  lmieu  23855  lmiinv  23863  clwlkisclwwlklem2a  24489  eupath2lem2  24682  3vfriswmgralem  24708  frgrawopreg  24754  2spotdisj  24766  2spotiundisj  24767  2spotmdisj  24773  frgrareg  24822  ex-natded5.7  24837  ex-natded5.13  24841  ex-natded9.20  24843  ex-natded9.20-2  24844  esumsn  27740  meascnbl  27858  signsplypnf  28175  signstfvn  28194  fprod  28678  binomfallfaclem2  28767  sltres  29029  nobndup  29065  dfrdg4  29205  outsideoftr  29384  lineunray  29402  dvtanlem  29669  ftc1anclem3  29697  dvasin  29708  areacirclem4  29715  smprngopr  30080  tsim2  30170  tsim3  30171  tsbi1  30172  tsbi2  30173  tsbi3  30174  tsan2  30181  tsan3  30182  tsor2  30187  tsor3  30188  pell1234qrdich  30429  acongtr  30548  acongrep  30550  jm2.23  30570  jm2.25  30573  fnwe2lem3  30630  kelac2lem  30642  refsum2cnlem1  31018  fmul01lt1lem1  31162  limciccioolb  31191  limcicciooub  31207  cncfiooicclem1  31260  wallispilem3  31395  fourierdlem35  31470  fourierdlem80  31515  fourierdlem101  31536  2reu4a  31689  otiunsndisjX  31796  usgvad2edg  31906  altgsumbcALT  32038  lindslinindsimp1  32157  lindszr  32169  zlmodzxznm  32197  bj-animorr  33236  bj-animorlr  33237  lkrshpor  33922  cdleme22b  35155  tendoex  35789  lcfrlem9  36365
  Copyright terms: Public domain W3C validator