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 23545. (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  513  pm1.5  519  cases2  958  somin1  5231  soxp  6684  fowdom  7782  unxpwdom2  7799  fin1a2lem11  8575  axdc3lem2  8616  gchdomtri  8792  hargch  8836  alephgch  8837  nn1m1nn  10338  nnnegz  10645  rpneg  11016  ltpnf  11098  mnflt  11100  xrlttri  11112  xmulpnf1  11233  iccsplit  11414  elfznelfzo  11626  bc0k  12083  bcpasc  12093  hashv01gt1  12112  pr2pwpr  12179  hashtpg  12182  hashf1  12206  ffz0iswrd  12251  wrdsymb0  12255  ccatsymb  12277  fsum  13193  fsumsplit  13212  fsumdvds  13572  sumhash  13954  4sqlem17  14018  vdwlem6  14043  ram0  14079  cshwsidrepswmod0  14117  cshwsdisj  14121  mreexfidimd  14584  psgnunilem1  15992  psgnunilem5  15993  gsummulg  16430  srgbinomlem3  16630  drngnidl  17289  cnsubrg  17832  en2top  18549  fctop  18567  cctop  18569  metusttoOLD  20091  metustto  20092  pmltpclem2  20892  itg1addlem5  21137  itg10a  21147  dvne0  21442  plyeq0lem  21637  plymullem1  21641  aalioulem4  21760  aalioulem5  21761  aaliou2b  21766  ang180lem3  22166  basellem2  22378  musumsum  22491  dchrhash  22569  lgsdir2lem5  22625  rpvmasumlem  22695  rpvmasum2  22720  pntlemj  22811  tgcolg  22946  tgbtwnconn1  22962  tgbtwnconn2  22963  colmid  23031  eupath2lem2  23534  ex-natded5.7  23553  ex-natded5.13  23557  ex-natded9.20  23559  ex-natded9.20-2  23560  esumsn  26451  meascnbl  26569  signsplypnf  26881  signstfvn  26900  fprod  27383  binomfallfaclem2  27472  sltres  27734  nobndup  27770  dfrdg4  27910  outsideoftr  28089  lineunray  28107  dvtanlem  28366  ftc1anclem3  28394  dvasin  28405  areacirclem4  28412  smprngopr  28777  tsim2  28867  tsim3  28868  tsbi1  28869  tsbi2  28870  tsbi3  28871  tsan2  28878  tsan3  28879  tsor2  28884  tsor3  28885  pell1234qrdich  29127  acongtr  29246  acongrep  29248  jm2.23  29270  jm2.25  29273  fnwe2lem3  29330  kelac2lem  29342  refsum2cnlem1  29684  fmul01lt1lem1  29690  wallispilem3  29787  2reu4a  29938  otsndisj  30056  otiunsndisj  30057  otiunsndisjX  30058  nn01to3  30112  hashrabsn01  30157  clwlkisclwwlklem2a  30372  3vfriswmgralem  30521  frgrawopreg  30567  2spotdisj  30579  2spotiundisj  30580  2spotmdisj  30586  frgrareg  30635  altgsumbcALT  30667  lindslinindsimp1  30832  lindszr  30844  zlmodzxznm  30880  lkrshpor  32474  cdleme22b  33707  tendoex  34341  lcfrlem9  34917
  Copyright terms: Public domain W3C validator