Theorem ori 230

Description: Infer implication from disjunction.

Hypothesis

Ref	Expression
ori.1	|- (ph \/ ps)

Assertion

Ref	Expression
ori	|- (-. ph -> ps)

Proof of Theorem ori

Step	Hyp	Ref	Expression
1		ori.1	. 2 |- (ph \/ ps)
2		df-or 224	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3	1, 2	mpbi 189	1 |- (-. ph -> ps)

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222

This theorem is referenced by:  3ori 883  moexex 1436  mo2icl 1919  mosubopt 2799  onuninsuc 3103  dff2 3808  omelon 4609  rankxpsuc 4695  brdom3 4781  cardom 4805  cardlim 4831  unialeph 4875  nneo 6152  absgt0 6786  bcpasc 6915  sinhalfpilem 8617

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 147  df-or 224

Copyright terms: Public domain