Theorem orri 231

Description: Infer implication from disjunction.

Hypothesis

Ref	Expression
orri.1	|- (-. ph -> ps)

Assertion

Ref	Expression
orri	|- (ph \/ ps)

Proof of Theorem orri

Step	Hyp	Ref	Expression
1		orri.1	. 2 |- (-. ph -> ps)
2		df-or 224	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3	1, 2	mpbir 190	1 |- (ph \/ ps)

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

This theorem is referenced by:  pm2.25 253  pm3.12 316  exmid 653  pm2.1 654  pm2.13 655  pm2.26 657  pm5.11 660  pm5.12 661  pm5.13 662  pm5.14 663  pm5.15 664  pm5.54 681  exmo 1409  erdisj 4270  letri 5558  posex 5856

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