Theorem orri 201

Description: Inference from disjunction definition.

Hypothesis

Ref	Expression
orri.1	⊢ (¬ φ → ψ)

Assertion

Ref	Expression
orri	⊢ (φ ∨ ψ)

Proof of Theorem orri

Step	Hyp	Ref	Expression
1		orri.1	. 2 ⊢ (¬ φ → ψ)
2		df-or 197	. 2 ⊢ ((φ ∨ ψ) ↔ (¬ φ → ψ))
3	1, 2	mpbir 165	1 ⊢ (φ ∨ ψ)

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