Theorem orri 201

Description: Inference from disjunction definition.

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 197	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3	1, 2	mpbir 165	1 |- (ph \/ ps)

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195

This theorem is referenced by:  exmid 494  pm2.1 495  exmo 1042  snsspr 1853  dmsnsn0 2544  erdisj 3223  kmlem2 3581  leidt 4293  letri 4306  posex 4422  nnleltp1t 4448  nneo 4719

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org