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

Theorem ord 726
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 724 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 711
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm2.8  812  orcanai  930  ax12  1535  swopo  4353  sotritrieq  4372  suc11g  4605  ordsoexmid  4610  nnsuc  4664  sotri2  5080  nnsucsssuc  6578  nntri2  6580  nntri1  6582  nnsseleq  6587  djulclb  7157  0ct  7209  exmidomniim  7243  omniwomnimkv  7269  elni2  7427  nlt1pig  7454  nngt1ne1  9071  zleloe  9419  zapne  9447  nneo  9476  zeo2  9479  fzocatel  10328  seqf1oglem1  10664  seqf1oglem2  10665  bitsinv1lem  12272  dfphi2  12542  prmdiv  12557  odzdvds  12568  pc2dvds  12653  fldivp1  12671  pcfac  12673  1arith  12690  4sqlem10  12710  plyaddlem1  15219  plymullem1  15220  gausslemma2dlem4  15541  lgseisenlem1  15547  bj-peano4  15891
  Copyright terms: Public domain W3C validator