HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem olci 291
Description: Deduction introducing a disjunct.
Hypothesis
Ref Expression
orci.1 |- ph
Assertion
Ref Expression
olci |- (ps \/ ph)

Proof of Theorem olci
StepHypRef Expression
1 orci.1 . 2 |- ph
2 olc 288 . 2 |- (ph -> (ps \/ ph))
31, 2ax-mp 7 1 |- (ps \/ ph)
Colors of variables: wff set class
Syntax hints:   \/ wo 238
This theorem is referenced by:  sucid 3558  unisn2 3610  kmlem2 5724  pnfxrOLD 6457  leid 6497  xrleid 6531  nnleltp1 6933  sin01bndlem2 8529  FTOid 13842
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 163  df-or 240
Copyright terms: Public domain