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

Theorem ord 642
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 640 . 2 ((ψ χ) → (¬ ψχ))
31, 2syl 14 1 (φ → (¬ ψχ))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm2.8  722  orcanai  836  ax-12  1399  swopo  4033  sotritrieq  4052  suc11g  4234  ordsoexmid  4239  nnsuc  4280  sotri2  4664  nnsucsssuc  6003  nntri2  6005  nntri1  6006  elni2  6291  nlt1pig  6318  nngt1ne1  7680  zleloe  8018  zapne  8041  nneo  8066  zeo2  8069  fzocatel  8771  bj-peano4  9008
  Copyright terms: Public domain W3C validator