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

Theorem olcd 383
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 21552. (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 382 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 378 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  pm2.48  390  pm2.49  391  orim12i  503  pm1.5  509  somin1  5203  soxp  6388  fowdom  7465  unxpwdom2  7482  fin1a2lem11  8216  axdc3lem2  8257  gchdomtri  8430  hargch  8478  alephgch  8479  nn1m1nn  9945  nnnegz  10210  rpneg  10566  ltpnf  10646  mnflt  10647  xrlttri  10657  xmulpnf1  10778  iccsplit  10954  elfznelfzo  11112  bc0k  11522  bcpasc  11532  hashv01gt1  11549  hashtpg  11611  hashf1  11626  fsum  12434  fsumsplit  12453  fsumdvds  12813  sumhash  13185  4sqlem17  13249  vdwlem6  13274  ram0  13310  mreexfidimd  13795  gsummulg  15457  drngnidl  16220  cnsubrg  16675  en2top  16966  fctop  16984  cctop  16986  metustto  18466  pmltpclem2  19206  itg1addlem5  19452  itg10a  19462  dvne0  19755  plyeq0lem  19989  plymullem1  19993  aalioulem4  20112  aalioulem5  20113  aaliou2b  20118  ang180lem3  20513  basellem2  20724  musumsum  20837  dchrhash  20915  lgsdir2lem5  20971  rpvmasumlem  21041  rpvmasum2  21066  pntlemj  21157  nbusgra  21299  eupath2lem2  21541  ex-natded5.7  21560  ex-natded5.13  21564  ex-natded9.20  21566  ex-natded9.20-2  21567  esumsn  24245  meascnbl  24360  fprod  25039  sltres  25335  nobndup  25371  dfrdg4  25506  outsideoftr  25770  lineunray  25788  dvreasin  25973  areacirclem5  25979  smprngopr  26346  pell1234qrdich  26608  acongtr  26727  acongrep  26729  jm2.23  26751  jm2.25  26754  fnwe2lem3  26811  kelac2lem  26824  psgnunilem1  27078  psgnunilem5  27079  refsum2cnlem1  27369  fmul01lt1lem1  27375  wallispilem3  27477  2reu4a  27628  frgra2v  27745  3vfriswmgralem  27750  frgrawopreg  27794  lkrshpor  29273  cdleme22b  30506  tendoex  31140  lcfrlem9  31716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator