Theorem orrd 203

Description: Deduction from disjunction definition.

Hypothesis

Ref	Expression
orrd.1	⊢ (φ → (¬ ψ → χ))

Assertion

Ref	Expression
orrd	⊢ (φ → (ψ ∨ χ))

Proof of Theorem orrd

Step	Hyp	Ref	Expression
1		orrd.1	. 2 ⊢ (φ → (¬ ψ → χ))
2		df-or 197	. 2 ⊢ ((ψ ∨ χ) ↔ (¬ ψ → χ))
3	1, 2	sylibr 175	1 ⊢ (φ → (ψ ∨ χ))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195

This theorem is referenced by:  olc 224  orc 225  pm2.48 230  sspss 1569  sssn 1852  pwpw0 1883  pwssun 1917  orduniorsuc 2337  unizlim 2364  ordzsl 2366  nn0suc 2395  fvclss 2907  entri 3645  iscard3 3693  psslinpr 3929  mul0or 4210  nnleltp1t 4448  h1datom 5483

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