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 25698. (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  4044  otsndisj  4726  otiunsndisj  4727  somin1  5253  soxp  6920  fowdom  8086  unxpwdom2  8103  fin1a2lem11  8838  axdc3lem2  8879  gchdomtri  9053  hargch  9097  alephgch  9098  nn1m1nn  10629  nn01to3  11257  rpneg  11332  ltpnf  11422  mnflt  11425  xrlttri  11438  xmulpnf1  11560  iccsplit  11763  elfznelfzo  12011  bc0k  12493  bcpasc  12503  hashv01gt1  12525  hashrabsn01  12549  hashf1  12615  pr2pwpr  12629  hashtpg  12632  ffz0iswrd  12681  ccatsymb  12714  fsum  13764  fsumsplit  13784  fprod  13973  binomfallfaclem2  14071  fsumdvds  14326  lcmfunsnlem1  14581  lcmfunsnlem2  14584  ncoprmlnprm  14648  sumhash  14804  4sqlem17OLD  14868  4sqlem17  14874  vdwlem6  14899  ram0  14943  cshwsidrepswmod0  15028  cshwsdisj  15032  mreexfidimd  15507  sgrp2nmndlem5  16614  psgnunilem1  17085  psgnunilem5  17086  gsummulg  17510  srgbinomlem3  17710  drngnidl  18388  gsummoncoe1  18833  cnsubrg  18963  pmatcoe1fsupp  19656  mp2pm2mplem4  19764  en2top  19932  fctop  19950  cctop  19952  metustto  21499  pmltpclem2  22281  itg1addlem5  22535  itg10a  22545  dvne0  22840  plyeq0lem  23032  plymullem1  23036  aalioulem4  23156  aalioulem5  23157  aaliou2b  23162  relogbf  23593  logblog  23594  ang180lem3  23605  basellem2  23871  musumsum  23984  dchrhash  24062  lgsdir2lem5  24118  rpvmasumlem  24188  rpvmasum2  24213  pntlemj  24304  tgcolg  24459  tgbtwnconn1  24480  tgbtwnconn2  24481  hlid  24514  hltr  24515  hlbtwn  24516  colmid  24590  lmieu  24682  lmiinv  24690  cgrahl  24723  cgracol  24724  clwlkisclwwlklem2a  25358  eupath2lem2  25551  3vfriswmgralem  25577  frgrawopreg  25622  2spotdisj  25634  2spotiundisj  25635  2spotmdisj  25641  frgrareg  25690  ex-natded5.7  25706  ex-natded5.13  25710  ex-natded9.20  25712  ex-natded9.20-2  25713  f1ocnt  28212  esumsnf  28724  meascnbl  28880  signsplypnf  29227  signstfvn  29246  sltres  30338  nobndup  30374  dfrdg4  30503  outsideoftr  30681  lineunray  30699  bj-animorr  30931  bj-animorlr  30932  dvtanlemOLD  31694  ftc1anclem3  31722  dvasin  31731  areacirclem4  31738  smprngopr  31988  tsbi1  32078  tsbi2  32079  lkrshpor  32381  cdleme22b  33616  tendoex  34250  lcfrlem9  34826  pell1234qrdich  35414  acongtr  35533  acongrep  35535  jm2.23  35556  jm2.25  35559  fnwe2lem3  35615  kelac2lem  35627  ifpim23g  35837  frege122d  35990  refsum2cnlem1  36997  fmul01lt1lem1  37233  limciccioolb  37272  sumnnodd  37281  limcicciooub  37288  wallispilem3  37497  fourierdlem35  37572  fourierdlem80  37617  fourierdlem101  37638  fourierswlem  37661  etransclem32  37697  etransclem35  37700  2reu4a  38000  nltle2tri  38105  icceuelpartlem  38138  evennodd  38162  oddneven  38163  otiunsndisjX  38377  usgvad2edg  38480  altgsumbcALT  38893  lindslinindsimp1  39009  lindszr  39021  zlmodzxznm  39049  elfzolborelfzop1  39076  blen1b  39159
  Copyright terms: Public domain W3C validator