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

Theorem olcd 382
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 20806. (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 381 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 377 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  pm2.48  389  pm2.49  390  orim12i  502  pm1.5  508  somin1  5095  soxp  6244  fowdom  7301  unxpwdom2  7318  fin1a2lem11  8052  axdc3lem2  8093  gchdomtri  8267  hargch  8315  alephgch  8316  nn1m1nn  9782  nnnegz  10043  rpneg  10399  ltpnf  10479  mnflt  10480  xrlttri  10489  xmulpnf1  10610  iccsplit  10784  bcpasc  11349  hashf1  11411  fsum  12209  fsumsplit  12228  fsumdvds  12588  sumhash  12960  4sqlem17  13024  vdwlem6  13049  0hashbc  13070  ram0  13085  mreexfidimd  13568  gsummulg  15230  drngnidl  15997  cnsubrg  16448  en2top  16739  fctop  16757  cctop  16759  pmltpclem2  18825  itg1addlem5  19071  itg10a  19081  dvne0  19374  plyeq0lem  19608  plymullem1  19612  aalioulem4  19731  aalioulem5  19732  aaliou2b  19737  ang180lem3  20125  basellem2  20335  musumsum  20448  dchrhash  20526  lgsdir2lem5  20582  rpvmasumlem  20652  rpvmasum2  20677  pntlemj  20768  ex-natded5.7  20814  ex-natded5.13  20818  ex-natded9.20  20820  ex-natded9.20-2  20821  esumsn  23452  meascnbl  23561  eupath2lem2  23917  fprod  24164  sltres  24389  nobndup  24425  dfrdg4  24560  outsideoftr  24824  lineunray  24842  dvreasin  25026  areacirclem5  25032  evpexun  25101  hdrmp  25809  partarelt2  26000  smprngopr  26780  pell1234qrdich  27049  acongtr  27168  acongrep  27170  jm2.23  27192  jm2.25  27195  fnwe2lem3  27252  kelac2lem  27265  psgnunilem1  27519  psgnunilem5  27520  refsum2cnlem1  27811  fmul01lt1lem1  27817  stoweidlem1  27853  wallispilem3  27919  2reu4a  28070  elfznelfzo  28213  hashtpg  28217  nbusgra  28277  frgra2v  28423  3vfriswmgralem  28428  lkrshpor  29919  cdleme22b  31152  tendoex  31786  lcfrlem9  32362
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 177  df-or 359
  Copyright terms: Public domain W3C validator