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

Theorem olci 406
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 391 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 383
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 197  df-or 385
This theorem is referenced by:  falortru  1509  sucidg  5772  kmlem2  8933  sornom  9059  leid  10093  pnf0xnn0  11330  xrleid  11943  xmul01  12056  bcn1  13056  odd2np1lem  15007  lcm0val  15250  lcmfunsnlem2lem1  15294  lcmfunsnlem2  15296  coprmprod  15318  coprmproddvdslem  15319  prmrec  15569  sratset  19124  srads  19126  m2detleib  20377  zclmncvs  22888  itg0  23486  itgz  23487  coemullem  23944  ftalem5  24737  chp1  24827  prmorcht  24838  pclogsum  24874  logexprlim  24884  bpos1  24942  pntpbnd1  25209  axlowdimlem16  25771  usgrexmpldifpr  26077  cusgrsizeindb1  26267  pthdlem2  26567  clwwlksn0  26807  ex-or  27166  plymulx0  30446  bj-0eltag  32666  bj-inftyexpidisj  32769  mblfinlem2  33118  volsupnfl  33125  ifpdfor  37329  ifpim1  37333  ifpnot  37334  ifpid2  37335  ifpim2  37336  ifpim1g  37366  ifpbi1b  37368  icccncfext  39435  fourierdlem103  39763  fourierdlem104  39764  etransclem24  39812  etransclem35  39823  abnotataxb  40417  dandysum2p2e4  40499  zlmodzxzldeplem  41605  aacllem  41880
  Copyright terms: Public domain W3C validator