Theorem ord 714

Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
ord.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
ord	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		pm2.53 712	. 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.8  800  orcanai  918  ax12  1500  swopo  4283  sotritrieq  4302  suc11g  4533  ordsoexmid  4538  nnsuc  4592  sotri2  5000  nnsucsssuc  6456  nntri2  6458  nntri1  6460  nnsseleq  6465  djulclb  7016  0ct  7068  exmidomniim  7101  omniwomnimkv  7127  elni2  7251  nlt1pig  7278  nngt1ne1  8888  zleloe  9234  zapne  9261  nneo  9290  zeo2  9293  fzocatel  10130  dfphi2  12148  prmdiv  12163  odzdvds  12173  pc2dvds  12257  fldivp1  12274  pcfac  12276  1arith  12293  4sqlem10  12313  bj-peano4  13797