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  1510  sucidg  5791  kmlem2  8958  sornom  9084  leid  10118  pnf0xnn0  11355  xrleid  11968  xmul01  12082  bcn1  13083  odd2np1lem  15045  lcm0val  15288  lcmfunsnlem2lem1  15332  lcmfunsnlem2  15334  coprmprod  15356  coprmproddvdslem  15357  prmrec  15607  sratset  19165  srads  19167  m2detleib  20418  zclmncvs  22929  itg0  23527  itgz  23528  coemullem  23987  ftalem5  24784  chp1  24874  prmorcht  24885  pclogsum  24921  logexprlim  24931  bpos1  24989  pntpbnd1  25256  axlowdimlem16  25818  usgrexmpldifpr  26131  cusgrsizeindb1  26327  pthdlem2  26645  clwwlksn0  26887  ex-or  27248  plymulx0  30598  bj-0eltag  32941  bj-inftyexpidisj  33068  mblfinlem2  33418  volsupnfl  33425  ifpdfor  37628  ifpim1  37632  ifpnot  37633  ifpid2  37634  ifpim2  37635  ifpim1g  37665  ifpbi1b  37667  icccncfext  39863  fourierdlem103  40189  fourierdlem104  40190  etransclem24  40238  etransclem35  40249  abnotataxb  40846  dandysum2p2e4  40928  sbgoldbo  41440  zlmodzxzldeplem  42052  aacllem  42312
  Copyright terms: Public domain W3C validator