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

Theorem olci 381
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
Hypothesis
Ref Expression
orci.1  |-  ph
Assertion
Ref Expression
olci  |-  ( ps  \/  ph )

Proof of Theorem olci
StepHypRef Expression
1 orci.1 . . 3  |-  ph
21a1i 11 . 2  |-  ( -. 
ps  ->  ph )
32orri 366 1  |-  ( ps  \/  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 358
This theorem is referenced by:  falortru  1351  sucidg  4651  kmlem2  8023  sornom  8149  leid  9161  xrleid  10735  xmul01  10838  bcn1  11596  odd2np1lem  12899  prmrec  13282  sratset  16247  srads  16249  itg0  19663  itgz  19664  coemullem  20160  ftalem5  20851  chp1  20942  prmorcht  20953  pclogsum  20991  logexprlim  21001  bpos1  21059  pntpbnd1  21272  usgraexmpldifpr  21411  cusgrasizeindb1  21472  vdgrf  21661  ex-or  21721  axlowdimlem16  25888  mblfinlem  26234  volsupnfl  26241  abnotataxb  27852  dandysum2p2e4  27910
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator