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

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
StepHypRef Expression
1 ord.1 . 2 (𝜑 → (𝜓𝜒))
2 pm2.53 717 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator