Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ord GIF version

Theorem ord 643
 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
StepHypRef Expression
1 ord.1 . 2 (𝜑 → (𝜓𝜒))
2 pm2.53 641 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 629 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  pm2.8  723  orcanai  837  ax-12  1402  swopo  4043  sotritrieq  4062  suc11g  4281  ordsoexmid  4286  nnsuc  4338  sotri2  4722  nnsucsssuc  6071  nntri2  6073  nntri1  6074  nnsseleq  6079  elni2  6412  nlt1pig  6439  nngt1ne1  7948  zleloe  8292  zapne  8315  nneo  8341  zeo2  8344  fzocatel  9055  bj-peano4  10080
 Copyright terms: Public domain W3C validator