Theorem ord 719

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 717	. 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

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

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 610  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.8  805  orcanai  923  ax12  1505  swopo  4291  sotritrieq  4310  suc11g  4541  ordsoexmid  4546  nnsuc  4600  sotri2  5008  nnsucsssuc  6471  nntri2  6473  nntri1  6475  nnsseleq  6480  djulclb  7032  0ct  7084  exmidomniim  7117  omniwomnimkv  7143  elni2  7276  nlt1pig  7303  nngt1ne1  8913  zleloe  9259  zapne  9286  nneo  9315  zeo2  9318  fzocatel  10155  dfphi2  12174  prmdiv  12189  odzdvds  12199  pc2dvds  12283  fldivp1  12300  pcfac  12302  1arith  12319  4sqlem10  12339  bj-peano4  13990