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

Theorem ord 678
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 676 . 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 664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.8  759  orcanai  875  ax-12  1447  swopo  4124  sotritrieq  4143  suc11g  4363  ordsoexmid  4368  nnsuc  4420  sotri2  4816  nnsucsssuc  6235  nntri2  6237  nntri1  6239  nnsseleq  6244  djulclb  6726  exmidomniim  6776  elni2  6852  nlt1pig  6879  nngt1ne1  8428  zleloe  8767  zapne  8791  nneo  8819  zeo2  8822  fzocatel  9575  dfphi2  11278  bj-peano4  11496
  Copyright terms: Public domain W3C validator