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  1510  swopo  4300  sotritrieq  4319  suc11g  4550  ordsoexmid  4555  nnsuc  4609  sotri2  5018  nnsucsssuc  6483  nntri2  6485  nntri1  6487  nnsseleq  6492  djulclb  7044  0ct  7096  exmidomniim  7129  omniwomnimkv  7155  elni2  7288  nlt1pig  7315  nngt1ne1  8927  zleloe  9273  zapne  9300  nneo  9329  zeo2  9332  fzocatel  10169  dfphi2  12187  prmdiv  12202  odzdvds  12212  pc2dvds  12296  fldivp1  12313  pcfac  12315  1arith  12332  4sqlem10  12352  bj-peano4  14276