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

Theorem ord 676
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 674 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.8  757  orcanai  871  ax-12  1443  swopo  4096  sotritrieq  4115  suc11g  4335  ordsoexmid  4340  nnsuc  4392  sotri2  4783  nnsucsssuc  6184  nntri2  6186  nntri1  6188  nnsseleq  6193  djulclb  6653  exmidomniim  6701  elni2  6775  nlt1pig  6802  nngt1ne1  8349  zleloe  8692  zapne  8716  nneo  8744  zeo2  8747  fzocatel  9498  dfphi2  10975  bj-peano4  11192
  Copyright terms: Public domain W3C validator