Theorem ord 731

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

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

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 620  ax-io 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  817  orcanai  935  ax12  1560  swopo  4403  sotritrieq  4422  suc11g  4655  ordsoexmid  4660  nnsuc  4714  sotri2  5134  nnsucsssuc  6660  nntri2  6662  nntri1  6664  nnsseleq  6669  djulclb  7254  0ct  7306  exmidomniim  7340  omniwomnimkv  7366  elni2  7534  nlt1pig  7561  nngt1ne1  9178  zleloe  9526  zapne  9554  nneo  9583  zeo2  9586  fzocatel  10445  seqf1oglem1  10782  seqf1oglem2  10783  bitsinv1lem  12524  dfphi2  12794  prmdiv  12809  odzdvds  12820  pc2dvds  12905  fldivp1  12923  pcfac  12925  1arith  12942  4sqlem10  12962  plyaddlem1  15474  plymullem1  15475  gausslemma2dlem4  15796  lgseisenlem1  15802  bj-peano4  16567