Theorem ord 725

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

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

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 616  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  811  orcanai  929  ax12  1526  swopo  4341  sotritrieq  4360  suc11g  4593  ordsoexmid  4598  nnsuc  4652  sotri2  5067  nnsucsssuc  6550  nntri2  6552  nntri1  6554  nnsseleq  6559  djulclb  7121  0ct  7173  exmidomniim  7207  omniwomnimkv  7233  elni2  7381  nlt1pig  7408  nngt1ne1  9025  zleloe  9373  zapne  9400  nneo  9429  zeo2  9432  fzocatel  10275  seqf1oglem1  10611  seqf1oglem2  10612  dfphi2  12388  prmdiv  12403  odzdvds  12414  pc2dvds  12499  fldivp1  12517  pcfac  12519  1arith  12536  4sqlem10  12556  plyaddlem1  14983  plymullem1  14984  gausslemma2dlem4  15305  lgseisenlem1  15311  bj-peano4  15601