Theorem ord 736

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.8  822  orcanai  940  ax12  1565  swopo  4453  sotritrieq  4472  suc11g  4706  ordsoexmid  4711  nnsuc  4765  sotri2  5188  nnsucsssuc  6769  nntri2  6771  nntri1  6773  nnsseleq  6778  djulclb  7401  0ct  7453  exmidomniim  7487  omniwomnimkv  7513  elni2  7687  nlt1pig  7714  nngt1ne1  9348  zleloe  9702  zapne  9730  nneo  9760  zeo2  9763  fzocatel  10634  seqf1oglem1  10977  seqf1oglem2  10978  bitsinv1lem  12753  dfphi2  13027  prmdiv  13042  odzdvds  13053  pc2dvds  13138  fldivp1  13156  pcfac  13158  1arith  13175  4sqlem10  13195  plyaddlem1  15973  plymullem1  15974  gausslemma2dlem4  16388  lgseisenlem1  16394  bj-peano4  17186