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 21664. (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  5229  soxp  6418  fowdom  7495  unxpwdom2  7512  fin1a2lem11  8246  axdc3lem2  8287  gchdomtri  8460  hargch  8508  alephgch  8509  nn1m1nn  9976  nnnegz  10241  rpneg  10597  ltpnf  10677  mnflt  10678  xrlttri  10688  xmulpnf1  10809  iccsplit  10985  elfznelfzo  11147  bc0k  11557  bcpasc  11567  hashv01gt1  11584  hashtpg  11646  hashf1  11661  fsum  12469  fsumsplit  12488  fsumdvds  12848  sumhash  13220  4sqlem17  13284  vdwlem6  13309  ram0  13345  mreexfidimd  13830  gsummulg  15492  drngnidl  16255  cnsubrg  16714  en2top  17005  fctop  17023  cctop  17025  metusttoOLD  18540  metustto  18541  pmltpclem2  19299  itg1addlem5  19545  itg10a  19555  dvne0  19848  plyeq0lem  20082  plymullem1  20086  aalioulem4  20205  aalioulem5  20206  aaliou2b  20211  ang180lem3  20606  basellem2  20817  musumsum  20930  dchrhash  21008  lgsdir2lem5  21064  rpvmasumlem  21134  rpvmasum2  21159  pntlemj  21250  eupath2lem2  21653  ex-natded5.7  21672  ex-natded5.13  21676  ex-natded9.20  21678  ex-natded9.20-2  21679  esumsn  24409  meascnbl  24526  sibfof  24607  fprod  25220  binomfallfaclem2  25307  sltres  25532  nobndup  25568  dfrdg4  25703  outsideoftr  25967  lineunray  25985  dvreasin  26179  areacirclem5  26185  smprngopr  26552  pell1234qrdich  26814  acongtr  26933  acongrep  26935  jm2.23  26957  jm2.25  26960  fnwe2lem3  27017  kelac2lem  27030  psgnunilem1  27284  psgnunilem5  27285  refsum2cnlem1  27575  fmul01lt1lem1  27581  wallispilem3  27683  2reu4a  27834  otsndisj  27953  otiunsndisj  27954  otiunsndisjX  27955  frgra2v  28103  3vfriswmgralem  28108  frgrawopreg  28152  2spotdisj  28164  2spotiundisj  28165  2spotmdisj  28171  lkrshpor  29590  cdleme22b  30823  tendoex  31457  lcfrlem9  32033
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