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

Theorem olci 405
 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 390 1 (𝜓𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∨ wo 382 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 196  df-or 384 This theorem is referenced by:  falortru  1503  sucidg  5720  kmlem2  8856  sornom  8982  leid  10012  pnf0xnn0  11247  xrleid  11859  xmul01  11969  bcn1  12962  odd2np1lem  14902  lcm0val  15145  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  coprmprod  15213  coprmproddvdslem  15214  prmrec  15464  sratset  19005  srads  19007  m2detleib  20256  zclmncvs  22756  itg0  23352  itgz  23353  coemullem  23810  ftalem5  24603  chp1  24693  prmorcht  24704  pclogsum  24740  logexprlim  24750  bpos1  24808  pntpbnd1  25075  axlowdimlem16  25637  usgraexmpldifpr  25928  cusgrasizeindb1  26000  vdgrf  26425  ex-or  26670  plymulx0  29950  bj-0eltag  32159  bj-inftyexpidisj  32274  mblfinlem2  32617  volsupnfl  32624  ifpdfor  36828  ifpim1  36832  ifpnot  36833  ifpid2  36834  ifpim2  36835  ifpim1g  36865  ifpbi1b  36867  icccncfext  38773  fourierdlem103  39102  fourierdlem104  39103  etransclem24  39151  etransclem35  39162  abnotataxb  39732  dandysum2p2e4  39814  cusgrsizeindb1  40666  pthdlem2  40974  clwwlksn0  41214  zlmodzxzldeplem  42081  aacllem  42356
 Copyright terms: Public domain W3C validator