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

Theorem ord 696
Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
ord.1  |-  ( ph  ->  ( ps  \/  ch ) )
Assertion
Ref Expression
ord  |-  ( ph  ->  ( -.  ps  ->  ch ) )

Proof of Theorem ord
StepHypRef Expression
1 ord.1 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
2 pm2.53 694 . 2  |-  ( ( ps  \/  ch )  ->  ( -.  ps  ->  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 680
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 587  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm2.8  782  orcanai  896  ax-12  1472  swopo  4196  sotritrieq  4215  suc11g  4440  ordsoexmid  4445  nnsuc  4497  sotri2  4904  nnsucsssuc  6354  nntri2  6356  nntri1  6358  nnsseleq  6363  djulclb  6906  0ct  6958  exmidomniim  6979  elni2  7086  nlt1pig  7113  nngt1ne1  8715  zleloe  9055  zapne  9079  nneo  9108  zeo2  9111  fzocatel  9927  dfphi2  11802  bj-peano4  12987
  Copyright terms: Public domain W3C validator