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

Theorem olcd 394
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 25795. (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 393 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 389 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 369
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 188  df-or 371
This theorem is referenced by:  pm2.48  401  pm2.49  402  orim12i  518  pm1.5  524  cases2  980  eqoreldif  3984  otsndisj  4668  otiunsndisj  4669  somin1  5195  soxp  6864  fowdom  8039  unxpwdom2  8056  fin1a2lem11  8791  axdc3lem2  8832  gchdomtri  9005  hargch  9049  alephgch  9050  nn1m1nn  10580  nn01to3  11208  rpneg  11283  ltpnf  11373  mnflt  11376  xrlttri  11389  xmulpnf1  11511  iccsplit  11716  elfznelfzo  11964  bc0k  12446  bcpasc  12456  hashv01gt1  12478  hashrabsn01  12502  hashf1  12568  pr2pwpr  12584  hashtpg  12589  ffz0iswrd  12642  ccatsymb  12675  fsum  13729  fsumsplit  13749  fprod  13938  binomfallfaclem2  14036  fsumdvds  14291  lcmfunsnlem1  14553  lcmfunsnlem2  14556  ncoprmlnprm  14620  sumhash  14784  4sqlem17OLD  14848  4sqlem17  14854  vdwlem6  14879  ram0  14923  cshwsidrepswmod0  15008  cshwsdisj  15012  mreexfidimd  15499  sgrp2nmndlem5  16606  psgnunilem1  17077  psgnunilem5  17078  gsummulg  17518  srgbinomlem3  17718  drngnidl  18396  gsummoncoe1  18841  cnsubrg  18971  pmatcoe1fsupp  19667  mp2pm2mplem4  19775  en2top  19943  fctop  19961  cctop  19963  metustto  21510  pmltpclem2  22342  itg1addlem5  22600  itg10a  22610  dvne0  22905  plyeq0lem  23106  plymullem1  23110  aalioulem4  23233  aalioulem5  23234  aaliou2b  23239  relogbf  23670  logblog  23671  ang180lem3  23682  basellem2  23950  musumsum  24063  dchrhash  24141  lgsdir2lem5  24197  rpvmasumlem  24267  rpvmasum2  24292  pntlemj  24383  tgcolg  24541  tgbtwnconn1  24562  tgbtwnconn2  24563  hlid  24596  hltr  24597  hlbtwn  24598  lnhl  24602  colmid  24675  hlpasch  24740  lmieu  24768  lmiinv  24776  cgrahl  24810  cgracol  24811  inaghl  24823  clwlkisclwwlklem2a  25455  eupath2lem2  25648  3vfriswmgralem  25674  frgrawopreg  25719  2spotdisj  25731  2spotiundisj  25732  2spotmdisj  25738  frgrareg  25787  ex-natded5.7  25803  ex-natded5.13  25807  ex-natded9.20  25809  ex-natded9.20-2  25810  f1ocnt  28326  esumsnf  28837  meascnbl  28993  signsplypnf  29391  signstfvn  29410  sltres  30502  nobndup  30538  dfrdg4  30667  outsideoftr  30845  lineunray  30863  bj-animorr  31095  bj-animorlr  31096  dvtanlemOLD  31898  ftc1anclem3  31926  dvasin  31935  areacirclem4  31942  smprngopr  32192  tsbi1  32282  tsbi2  32283  lkrshpor  32585  cdleme22b  33820  tendoex  34454  lcfrlem9  35030  pell1234qrdich  35620  acongtr  35741  acongrep  35743  jm2.23  35764  jm2.25  35767  fnwe2lem3  35823  kelac2lem  35835  ifpim23g  36052  frege122d  36265  refsum2cnlem1  37274  fmul01lt1lem1  37545  limciccioolb  37584  sumnnodd  37593  limcicciooub  37600  wallispilem3  37812  fourierdlem35  37888  fourierdlem80  37933  fourierdlem101  37954  fourierswlem  37977  etransclem32  38014  etransclem35  38017  2reu4a  38424  nltle2tri  38529  icceuelpartlem  38562  evennodd  38586  oddneven  38587  n0snor2el  38805  propeqop  38808  otiunsndisjX  38814  nbgrnvtx0  39155  usgvad2edg  39324  altgsumbcALT  39737  lindslinindsimp1  39853  lindszr  39865  zlmodzxznm  39893  elfzolborelfzop1  39919  blen1b  40002
  Copyright terms: Public domain W3C validator