MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  olci Structured version   Visualization version   GIF version

Theorem olci 404
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
Hypothesis
Ref Expression
orci.1 𝜑
Assertion
Ref Expression
olci (𝜓𝜑)

Proof of Theorem olci
StepHypRef Expression
1 orci.1 . . 3 𝜑
21a1i 11 . 2 𝜓𝜑)
32orri 389 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 381
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 195  df-or 383
This theorem is referenced by:  falortru  1502  sucidg  5706  kmlem2  8833  sornom  8959  leid  9984  xrleid  11818  xmul01  11926  bcn1  12917  odd2np1lem  14848  lcm0val  15091  lcmfunsnlem2lem1  15135  lcmfunsnlem2  15137  coprmprod  15159  coprmproddvdslem  15160  prmrec  15410  sratset  18951  srads  18953  m2detleib  20198  itg0  23269  itgz  23270  coemullem  23727  ftalem5  24520  chp1  24610  prmorcht  24621  pclogsum  24657  logexprlim  24667  bpos1  24725  pntpbnd1  24992  axlowdimlem16  25555  usgraexmpldifpr  25694  cusgrasizeindb1  25766  vdgrf  26191  ex-or  26436  plymulx0  29756  bj-0eltag  31962  bj-inftyexpidisj  32077  mblfinlem2  32420  volsupnfl  32427  ifpdfor  36631  ifpim1  36635  ifpnot  36636  ifpid2  36637  ifpim2  36638  ifpim1g  36668  ifpbi1b  36670  icccncfext  38577  fourierdlem103  38906  fourierdlem104  38907  etransclem24  38955  etransclem35  38966  abnotataxb  39536  dandysum2p2e4  39618  pnf0xnn0  40207  cusgrsizeindb1  40668  pthdlem2  40976  clwwlksn0  41216  zlmodzxzldeplem  42083  aacllem  42319
  Copyright terms: Public domain W3C validator