Theorem ord 726

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  812  orcanai  930  ax12  1535  swopo  4354  sotritrieq  4373  suc11g  4606  ordsoexmid  4611  nnsuc  4665  sotri2  5081  nnsucsssuc  6580  nntri2  6582  nntri1  6584  nnsseleq  6589  djulclb  7159  0ct  7211  exmidomniim  7245  omniwomnimkv  7271  elni2  7429  nlt1pig  7456  nngt1ne1  9073  zleloe  9421  zapne  9449  nneo  9478  zeo2  9481  fzocatel  10330  seqf1oglem1  10666  seqf1oglem2  10667  bitsinv1lem  12305  dfphi2  12575  prmdiv  12590  odzdvds  12601  pc2dvds  12686  fldivp1  12704  pcfac  12706  1arith  12723  4sqlem10  12743  plyaddlem1  15252  plymullem1  15253  gausslemma2dlem4  15574  lgseisenlem1  15580  bj-peano4  15928