Theorem ord 724

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  810  orcanai  928  ax12  1512  swopo  4307  sotritrieq  4326  suc11g  4557  ordsoexmid  4562  nnsuc  4616  sotri2  5027  nnsucsssuc  6493  nntri2  6495  nntri1  6497  nnsseleq  6502  djulclb  7054  0ct  7106  exmidomniim  7139  omniwomnimkv  7165  elni2  7313  nlt1pig  7340  nngt1ne1  8954  zleloe  9300  zapne  9327  nneo  9356  zeo2  9359  fzocatel  10199  dfphi2  12220  prmdiv  12235  odzdvds  12245  pc2dvds  12329  fldivp1  12346  pcfac  12348  1arith  12365  4sqlem10  12385  lgseisenlem1  14453  bj-peano4  14710