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

Theorem ord 642
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 640 . 2
31, 2syl 14 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wo 628
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm2.8  722  orcanai  836  ax-12  1399  swopo  4034  sotritrieq  4053  suc11g  4235  ordsoexmid  4240  nnsuc  4281  sotri2  4665  nnsucsssuc  6010  nntri2  6012  nntri1  6013  elni2  6298  nlt1pig  6325  nngt1ne1  7689  zleloe  8028  zapne  8051  nneo  8077  zeo2  8080  fzocatel  8785  bj-peano4  9343
  Copyright terms: Public domain W3C validator