Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ord 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  4034  sotritrieq  4053  suc11g  4235  ordsoexmid  4240  nnsuc  4281  sotri2  4665  nnsucsssuc  6010  nntri2  6012  nntri1  6013  elni2  6298  nlt1pig  6325  nngt1ne1  7729  zleloe  8068  zapne  8091  nneo  8117  zeo2  8120  fzocatel  8825  bj-peano4  9415
 Copyright terms: Public domain W3C validator