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

Theorem olci 863
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 859 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 844
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 210  df-or 845
This theorem is referenced by:  falortru  1577  opthhausdorff  5388  sucidg  6250  kmlem2  9562  sornom  9684  leid  10721  pnf0xnn0  11960  xrleid  12530  xmul01  12646  bcn1  13667  odd2np1lem  15678  lcm0val  15925  lcmfunsnlem2lem1  15969  lcmfunsnlem2  15971  coprmprod  15992  coprmproddvdslem  15993  prmrec  16245  smndex2dnrinv  18069  sratset  19942  srads  19944  m2detleib  21226  zclmncvs  23742  itg0  24372  itgz  24373  coemullem  24836  ftalem5  25651  chp1  25741  prmorcht  25752  pclogsum  25788  logexprlim  25798  bpos1  25856  addsqnreup  26016  pntpbnd1  26159  axlowdimlem16  26740  usgrexmpldifpr  27037  cusgrsizeindb1  27229  pthdlem2  27546  ex-or  28195  plymulx0  31835  signstfvn  31857  bj-0eltag  34318  bj-inftyexpidisj  34528  mblfinlem2  34995  volsupnfl  35002  12gcd5e1  39187  3lexlogpow5ineq2  39238  ifpdfor  40005  ifpim1  40009  ifpnot  40010  ifpid2  40011  ifpim2  40012  ifpim1g  40041  ifpbi1b  40043  icccncfext  42371  fourierdlem103  42693  fourierdlem104  42694  etransclem24  42742  etransclem35  42753  abnotataxb  43351  dandysum2p2e4  43433  paireqne  43870  sbgoldbo  44147  zlmodzxzldeplem  44748  line2x  44998  aacllem  45159
  Copyright terms: Public domain W3C validator