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

Theorem ord 698
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 696 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 682
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 589  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm2.8  784  orcanai  898  ax-12  1474  swopo  4198  sotritrieq  4217  suc11g  4442  ordsoexmid  4447  nnsuc  4499  sotri2  4906  nnsucsssuc  6356  nntri2  6358  nntri1  6360  nnsseleq  6365  djulclb  6908  0ct  6960  exmidomniim  6981  elni2  7090  nlt1pig  7117  nngt1ne1  8723  zleloe  9069  zapne  9093  nneo  9122  zeo2  9125  fzocatel  9944  dfphi2  11823  bj-peano4  13080
  Copyright terms: Public domain W3C validator