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

Theorem ord 725
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 723 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 709
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 710
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm2.8  811  orcanai  929  ax12  1534  swopo  4352  sotritrieq  4371  suc11g  4604  ordsoexmid  4609  nnsuc  4663  sotri2  5079  nnsucsssuc  6577  nntri2  6579  nntri1  6581  nnsseleq  6586  djulclb  7156  0ct  7208  exmidomniim  7242  omniwomnimkv  7268  elni2  7426  nlt1pig  7453  nngt1ne1  9070  zleloe  9418  zapne  9446  nneo  9475  zeo2  9478  fzocatel  10326  seqf1oglem1  10662  seqf1oglem2  10663  bitsinv1lem  12243  dfphi2  12513  prmdiv  12528  odzdvds  12539  pc2dvds  12624  fldivp1  12642  pcfac  12644  1arith  12661  4sqlem10  12681  plyaddlem1  15190  plymullem1  15191  gausslemma2dlem4  15512  lgseisenlem1  15518  bj-peano4  15853
  Copyright terms: Public domain W3C validator