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

Theorem ord 676
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 674 . 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 662
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 578  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.8  757  orcanai  871  ax-12  1443  swopo  4069  sotritrieq  4088  suc11g  4308  ordsoexmid  4313  nnsuc  4364  sotri2  4752  nnsucsssuc  6136  nntri2  6138  nntri1  6140  nnsseleq  6145  elni2  6566  nlt1pig  6593  nngt1ne1  8140  zleloe  8479  zapne  8503  nneo  8531  zeo2  8534  fzocatel  9285  bj-peano4  10908
  Copyright terms: Public domain W3C validator