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 23610. (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  516  pm1.5  522  cases2  963  somin1  5234  soxp  6685  fowdom  7786  unxpwdom2  7803  fin1a2lem11  8579  axdc3lem2  8620  gchdomtri  8796  hargch  8840  alephgch  8841  nn1m1nn  10342  nnnegz  10649  rpneg  11020  ltpnf  11102  mnflt  11104  xrlttri  11116  xmulpnf1  11237  iccsplit  11418  elfznelfzo  11630  bc0k  12087  bcpasc  12097  hashv01gt1  12116  pr2pwpr  12183  hashtpg  12186  hashf1  12210  ffz0iswrd  12255  wrdsymb0  12259  ccatsymb  12281  fsum  13197  fsumsplit  13216  fsumdvds  13576  sumhash  13958  4sqlem17  14022  vdwlem6  14047  ram0  14083  cshwsidrepswmod0  14121  cshwsdisj  14125  mreexfidimd  14588  psgnunilem1  15999  psgnunilem5  16000  gsummulg  16438  srgbinomlem3  16640  drngnidl  17311  cnsubrg  17873  en2top  18590  fctop  18608  cctop  18610  metusttoOLD  20132  metustto  20133  pmltpclem2  20933  itg1addlem5  21178  itg10a  21188  dvne0  21483  plyeq0lem  21678  plymullem1  21682  aalioulem4  21801  aalioulem5  21802  aaliou2b  21807  ang180lem3  22207  basellem2  22419  musumsum  22532  dchrhash  22610  lgsdir2lem5  22666  rpvmasumlem  22736  rpvmasum2  22761  pntlemj  22852  tgcolg  22988  tgbtwnconn1  23007  tgbtwnconn2  23008  colmid  23082  eupath2lem2  23599  ex-natded5.7  23618  ex-natded5.13  23622  ex-natded9.20  23624  ex-natded9.20-2  23625  esumsn  26515  meascnbl  26633  signsplypnf  26951  signstfvn  26970  fprod  27454  binomfallfaclem2  27543  sltres  27805  nobndup  27841  dfrdg4  27981  outsideoftr  28160  lineunray  28178  dvtanlem  28441  ftc1anclem3  28469  dvasin  28480  areacirclem4  28487  smprngopr  28852  tsim2  28942  tsim3  28943  tsbi1  28944  tsbi2  28945  tsbi3  28946  tsan2  28953  tsan3  28954  tsor2  28959  tsor3  28960  pell1234qrdich  29202  acongtr  29321  acongrep  29323  jm2.23  29345  jm2.25  29348  fnwe2lem3  29405  kelac2lem  29417  refsum2cnlem1  29759  fmul01lt1lem1  29765  wallispilem3  29862  2reu4a  30013  otsndisj  30131  otiunsndisj  30132  otiunsndisjX  30133  nn01to3  30187  hashrabsn01  30232  clwlkisclwwlklem2a  30447  3vfriswmgralem  30596  frgrawopreg  30642  2spotdisj  30654  2spotiundisj  30655  2spotmdisj  30661  frgrareg  30710  altgsumbcALT  30750  gsummoncoe1  30843  pmatcoe1fsupp  30892  mp2pm2mplem4  30919  lindslinindsimp1  30991  lindszr  31003  zlmodzxznm  31039  bj-animorr  32074  bj-animorlr  32075  lkrshpor  32752  cdleme22b  33985  tendoex  34619  lcfrlem9  35195
  Copyright terms: Public domain W3C validator