Theorem ord 714

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 712	. 2 |- ( ( ps \/ ch ) -> ( -. ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( -. ps -> ch ) )

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

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 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.8  800  orcanai  914  ax-12  1490  swopo  4236  sotritrieq  4255  suc11g  4480  ordsoexmid  4485  nnsuc  4537  sotri2  4944  nnsucsssuc  6396  nntri2  6398  nntri1  6400  nnsseleq  6405  djulclb  6948  0ct  7000  exmidomniim  7021  omniwomnimkv  7049  elni2  7146  nlt1pig  7173  nngt1ne1  8779  zleloe  9125  zapne  9149  nneo  9178  zeo2  9181  fzocatel  10007  dfphi2  11932  bj-peano4  13324