Theorem ord 713

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

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

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 604  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.8  799  orcanai  913  ax-12  1489  swopo  4228  sotritrieq  4247  suc11g  4472  ordsoexmid  4477  nnsuc  4529  sotri2  4936  nnsucsssuc  6388  nntri2  6390  nntri1  6392  nnsseleq  6397  djulclb  6940  0ct  6992  exmidomniim  7013  elni2  7122  nlt1pig  7149  nngt1ne1  8755  zleloe  9101  zapne  9125  nneo  9154  zeo2  9157  fzocatel  9976  dfphi2  11896  bj-peano4  13153