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  918  ax12  1500  swopo  4284  sotritrieq  4303  suc11g  4534  ordsoexmid  4539  nnsuc  4593  sotri2  5001  nnsucsssuc  6460  nntri2  6462  nntri1  6464  nnsseleq  6469  djulclb  7020  0ct  7072  exmidomniim  7105  omniwomnimkv  7131  elni2  7255  nlt1pig  7282  nngt1ne1  8892  zleloe  9238  zapne  9265  nneo  9294  zeo2  9297  fzocatel  10134  dfphi2  12152  prmdiv  12167  odzdvds  12177  pc2dvds  12261  fldivp1  12278  pcfac  12280  1arith  12297  4sqlem10  12317  bj-peano4  13837