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 654  pm2.1 655  pm2.13 656  pm2.26 658  pm5.11 661  pm5.12 662  pm5.13 663  pm5.14 664  pm5.15 665  pm5.54 682  exmo 1415  erdisj 4279  letri 5568  posex 5866

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