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

Theorem ord 713
 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 711 . 2 ((𝜓𝜒) → (¬ 𝜓𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓𝜒))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 697 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 604  ax-io 698 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm2.8  799  orcanai  913  ax-12  1489  swopo  4223  sotritrieq  4242  suc11g  4467  ordsoexmid  4472  nnsuc  4524  sotri2  4931  nnsucsssuc  6381  nntri2  6383  nntri1  6385  nnsseleq  6390  djulclb  6933  0ct  6985  exmidomniim  7006  elni2  7115  nlt1pig  7142  nngt1ne1  8748  zleloe  9094  zapne  9118  nneo  9147  zeo2  9150  fzocatel  9969  dfphi2  11885  bj-peano4  13142
 Copyright terms: Public domain W3C validator