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

Theorem olcd 383
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IL ( \/ insertion left), see natded 21703. (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  5262  soxp  6451  fowdom  7531  unxpwdom2  7548  fin1a2lem11  8282  axdc3lem2  8323  gchdomtri  8496  hargch  8544  alephgch  8545  nn1m1nn  10012  nnnegz  10277  rpneg  10633  ltpnf  10713  mnflt  10714  xrlttri  10724  xmulpnf1  10845  iccsplit  11021  elfznelfzo  11184  bc0k  11594  bcpasc  11604  hashv01gt1  11621  hashtpg  11683  hashf1  11698  fsum  12506  fsumsplit  12525  fsumdvds  12885  sumhash  13257  4sqlem17  13321  vdwlem6  13346  ram0  13382  mreexfidimd  13867  gsummulg  15529  drngnidl  16292  cnsubrg  16751  en2top  17042  fctop  17060  cctop  17062  metusttoOLD  18579  metustto  18580  pmltpclem2  19338  itg1addlem5  19584  itg10a  19594  dvne0  19887  plyeq0lem  20121  plymullem1  20125  aalioulem4  20244  aalioulem5  20245  aaliou2b  20250  ang180lem3  20645  basellem2  20856  musumsum  20969  dchrhash  21047  lgsdir2lem5  21103  rpvmasumlem  21173  rpvmasum2  21198  pntlemj  21289  eupath2lem2  21692  ex-natded5.7  21711  ex-natded5.13  21715  ex-natded9.20  21717  ex-natded9.20-2  21718  esumsn  24448  meascnbl  24565  sibfof  24646  fprod  25259  binomfallfaclem2  25348  sltres  25611  nobndup  25647  dfrdg4  25787  outsideoftr  26055  lineunray  26073  ftc1anclem3  26272  dvreasin  26280  areacirclem5  26286  smprngopr  26653  pell1234qrdich  26915  acongtr  27034  acongrep  27036  jm2.23  27058  jm2.25  27061  fnwe2lem3  27118  kelac2lem  27130  psgnunilem1  27384  psgnunilem5  27385  refsum2cnlem1  27675  fmul01lt1lem1  27681  wallispilem3  27783  2reu4a  27934  otsndisj  28055  otiunsndisj  28056  otiunsndisjX  28057  wrdsymb0  28147  ccatsymb  28152  cshwssizelem2  28244  cshwsdisj  28248  frgra2v  28326  3vfriswmgralem  28331  frgrawopreg  28375  2spotdisj  28387  2spotiundisj  28388  2spotmdisj  28394  lkrshpor  29842  cdleme22b  31075  tendoex  31709  lcfrlem9  32285
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