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

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
StepHypRef Expression
1 ord.1 . 2 (𝜑 → (𝜓𝜒))
2 pm2.53 712 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff set class
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  914  ax12  1492  swopo  4269  sotritrieq  4288  suc11g  4519  ordsoexmid  4524  nnsuc  4578  sotri2  4986  nnsucsssuc  6442  nntri2  6444  nntri1  6446  nnsseleq  6451  djulclb  7002  0ct  7054  exmidomniim  7087  omniwomnimkv  7113  elni2  7237  nlt1pig  7264  nngt1ne1  8874  zleloe  9220  zapne  9244  nneo  9273  zeo2  9276  fzocatel  10108  dfphi2  12111  prmdiv  12126  odzdvds  12136  bj-peano4  13627
  Copyright terms: Public domain W3C validator