Theorem ord 729

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

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

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 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  815  orcanai  933  ax12  1558  swopo  4397  sotritrieq  4416  suc11g  4649  ordsoexmid  4654  nnsuc  4708  sotri2  5126  nnsucsssuc  6646  nntri2  6648  nntri1  6650  nnsseleq  6655  djulclb  7233  0ct  7285  exmidomniim  7319  omniwomnimkv  7345  elni2  7512  nlt1pig  7539  nngt1ne1  9156  zleloe  9504  zapne  9532  nneo  9561  zeo2  9564  fzocatel  10417  seqf1oglem1  10753  seqf1oglem2  10754  bitsinv1lem  12488  dfphi2  12758  prmdiv  12773  odzdvds  12784  pc2dvds  12869  fldivp1  12887  pcfac  12889  1arith  12906  4sqlem10  12926  plyaddlem1  15437  plymullem1  15438  gausslemma2dlem4  15759  lgseisenlem1  15765  bj-peano4  16401