Theorem ord 643

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

Step	Hyp	Ref	Expression
1		ord.1	. 2 |- ( ph -> ( ps \/ ch ) )
2		pm2.53 641	. 2 |- ( ( ps \/ ch ) -> ( -. ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( -. ps -> ch ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 629

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 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.8  723  orcanai  837  ax-12  1402  swopo  4043  sotritrieq  4062  suc11g  4281  ordsoexmid  4286  nnsuc  4338  sotri2  4722  nnsucsssuc  6071  nntri2  6073  nntri1  6074  nnsseleq  6079  elni2  6412  nlt1pig  6439  nngt1ne1  7948  zleloe  8292  zapne  8315  nneo  8341  zeo2  8344  fzocatel  9055  bj-peano4  10080