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  1523  swopo  4321  sotritrieq  4340  suc11g  4571  ordsoexmid  4576  nnsuc  4630  sotri2  5041  nnsucsssuc  6511  nntri2  6513  nntri1  6515  nnsseleq  6520  djulclb  7072  0ct  7124  exmidomniim  7157  omniwomnimkv  7183  elni2  7331  nlt1pig  7358  nngt1ne1  8972  zleloe  9318  zapne  9345  nneo  9374  zeo2  9377  fzocatel  10217  dfphi2  12238  prmdiv  12253  odzdvds  12263  pc2dvds  12347  fldivp1  12364  pcfac  12366  1arith  12383  4sqlem10  12403  lgseisenlem1  14847  bj-peano4  15104
  Copyright terms: Public domain W3C validator